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,g:(n).
Thm* (
i:n. f(i) = g(i)) 
sum(f(x) | x < n) = sum(g(x) | x < n)| Theorem | Name |
| 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] |
| cites the following: | |
| n:, f,g:(n).
Thm* ( i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n) | [sum_functionality] |