n:
, f:(n
), m:n.
Thm* (
x:n. 
x = m 
f(x) = 0) sum(f(x) | x < n) = f(m)n:, f:(n), m:n.
Thm* sum(f(x) | x < n) = f(m)+sum(if x=
m
0 else f(x) fi | x < n)n:, f:(n). (x:n. f(x) = 0) sum(f(x) | x < n) = 0| Rank | Theorem | Name |
| 2 | n:, f:(n), m:n.
Thm* ( x:n. x = m f(x) = 0) sum(f(x) | x < n) = f(m) | [singleton_support_sum] |
| cites the following: | ||
| 1 | n:, f:(n), m:n.
Thm* sum(f(x) | x < n) = f(m)+sum(if x= m 0 else f(x) fi | x < n) | [isolate_summand] |
| 1 | n:, f:(n). (x:n. f(x) = 0) sum(f(x) | x < n) = 0 | [empty_support] |