n,m:
, f,g:(n
m
), d:.
Thm* sum(f(x,y)-g(x,y) | x < n; y < m) = d
Thm*
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)+d
n:, f,g:(n).
Thm* (
i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n)n:, f,g:(n), d:.
Thm* sum(f(x)-g(x) | x < n) = d
sum(f(x) | x < n) = sum(g(x) | x < n)+d