f:(A
A), u:A. f(u) = u 
(i:
. f{
i}(u) = u)f:(AA), x:A. f{0}(x) = xf:(AA), i:
, x:A. f{i}(x) = f(f{i-1}(x))| Theorem | Name |
| f:(AA), u:A. f(u) = u (i:. f{i}(u) = u) | [compose_iter_point_id] |
| 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] |