Some positive iteration of any finite permutation is the identity function.

At: iter perm cycles uniform2

  k:, f:(k inj k). i:. f{i} = Id  kk

By:	SimilarTo Thm*  k:, f:(k inj k). i:. u:k. f{i}(u) = u ...w

1

1. k :  2. f : k inj k 3. i:. u:k. f{i}(u) = u   i:. f{i} = Id  kk

3 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html