x:A, f:(A
A), i,j,k:
. k = i
j 
f{
i}{j}(x) = f{k}(x) 
Af:(AA), x:A. f{0}(x) = xf:(AA). f{0} = Idi:. Id{i} = Id AAa,b:
, n:. a
b nanbf:(AA), i:
, x:A. f{i}(x) = f(f{i-1}(x))f:(AA), k:, i:{0...k}. f{k} = f{i} o f{k-i}| Rank | Theorem | Name |
| 4 | x:A, f:(AA), i,j,k:. k = ij f{i}{j}(x) = f{k}(x) A | [compose_iter_prod] |
| cites the following: | ||
| 0 | f:(AA), x:A. f{0}(x) = x | [compose_iter_zero] |
| 1 | f:(AA). f{0} = Id | [compose_iter_zero_id] |
| 2 | i:. Id{i} = Id AA | [compose_iter_id] |
| 0 | a,b:, n:. ab nanb | [mul_preserves_le] |
| 0 | f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x)) | [compose_iter_pos] |
| 3 | f:(AA), k:, i:{0...k}. f{k} = f{i} o f{k-i} | [compose_iter_sum_comp_rw] |