f:(A
A), i:
, x:A. f{
i}(x) = f{i-1}(f(x))f:(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 | f:(AA), i:, x:A. f{i}(x) = f{i-1}(f(x)) | [compose_iter_pos2] |
| cites the following: | ||
| 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] |