n,m:
, f:(n
m
), p:(nn), q:(mm).
Thm* Bij(
n; n; p)
Thm*
Thm* Bij(
m; m; q)
Thm*
Thm* sum(f(p(x),q(y)) | x < n; y < m) = sum(f(x,y) | x < n; y < m)
n:, f,g:(n).
Thm* (
i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n)n:, f:(n), p:(nn).
Thm* Bij(
n; n; p) sum(f(p(x)) | x < n) = sum(f(x) | x < n)