i:
. Id{
i} = Id 
A
Af:(AA). f{0} = Idf:(AA), i:
. f{i} = f o f{i-1}f:(AB). Id o f = f AB| Rank | Theorem | Name |
| 2 | i:. Id{i} = Id AA | [compose_iter_id] |
| cites the following: | ||
| 1 | f:(AA). f{0} = Id | [compose_iter_zero_id] |
| 1 | f:(AA), i:. f{i} = f o f{i-1} | [compose_iter_pos_comp] |
| 0 | f:(AB). Id o f = f AB | [comp_id_l_version2] |