is mentioned by

Thm* n,m:, f:(nm), 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)	[permute_double_sum]
Thm* n:, f:(n), p:(nn). Thm* Bij(n; n; p)  sum(f(p(x)) | x < n) = sum(f(x) | x < n)	[permute_sum]
Thm* k:, p:(kk). Bij(k; k; p)  (L:(k-1) List. p = compose_flips(L))	[permute_by_flips]
Thm* f,g:(TT). Bij(T; T; f)  Bij(T; T; g)  Bij(T; T; f o g)	[compose_bij]

In prior sections: fun 1 mb nat

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html