k:
, f:(k inj
k), u:k. 
i:
. f{
i}(u) = um,k:, f:(m
k). k<m 
(x,y:m. x 
y & f(x) = f(y))x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x)) (i:. Inj(A; A; f{i}))| Rank | Theorem | Name |
| 4 | k:, f:(k inj k), u:k. i:. f{i}(u) = u | [compose_iter_inj_cycles] |
| cites the following: | ||
| 3 | m,k:, f:(mk). k<m (x,y:m. x y & f(x) = f(y)) | [pigeon_hole] |
| 2 | x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x)) | [compose_iter_sum_rw] |
| 2 | (i:. Inj(A; A; f{i})) | [compose_iter_injection] |