x:A, f:(A
A), i,j,k:
. k = i+j 
f{
i}(f{j}(x)) = f{k}(x)f:(AA), x:A. f{0}(x) = xf:(AA), i:
, x:A. f{i}(x) = f(f{i-1}(x))| Theorem | Name |
| x:A, f:(AA), i,j,k:. k = i+j f{i}(f{j}(x)) = f{k}(x) | [compose_iter_sum] |
| cites the following: | |
| f:(AA), x:A. f{0}(x) = x | [compose_iter_zero] |
| f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x)) | [compose_iter_pos] |