n:
, f:(n
), m,k:n.
Thm*
m = k
Thm*
Thm* (
x:n. x = m x = k f(x) = 0) sum(f(x) | x < n) = f(m)+f(k)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), m:n.
Thm* (
x:n. x = m f(x) = 0) sum(f(x) | x < n) = f(m)