(
i:
. Surj(A; A; f{
i}))f:(A
A). f{0} = Idf:(AA). f{1} = fx:A, f:(AA), i,j,k:. k = i+j f{i}(f{j}(x)) = f{k}(x)| Rank | Theorem | Name |
| 2 | (i:. Surj(A; A; f{i})) | [compose_iter_surjection] |
| cites the following: | ||
| 1 | f:(AA). f{0} = Id | [compose_iter_zero_id] |
| 0 | f:(AA). f{1} = f | [compose_iter_once] |
| 1 | x:A, f:(AA), i,j,k:. k = i+j f{i}(f{j}(x)) = f{k}(x) | [compose_iter_sum] |