n:
, f:(n
). (x:n. f(x) = 0) 
sum(f(x) | x < n) = 0n:, f,g:(n).
Thm* (
i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n)n:, a:. sum(a | x < n) = a
n| Theorem | Name |
| n:, f:(n). (x:n. f(x) = 0) sum(f(x) | x < n) = 0 | [empty_support] |
| 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] |
| n:, a:. sum(a | x < n) = an | [sum_constant] |