n:
, f:(n
), p:(nn).
Thm* Bij(
n; n; p) 
sum(f(p(x)) | x < n) = sum(f(x) | x < n)k:, p:(kk). Bij(k; k; p) (
L:(k-1) List. p = compose_flips(L))n:, f,g:(n).
Thm* (
i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n)n:, f:(n), i:(n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n)