x:A, f:(A
A), i,j:
. f{
i}{j}(x) = f{i
j}(x)x:A, f:(AA), i,j,k:. k = ij 
f{i}{j}(x) = f{k}(x) 
A| Rank | Theorem | Name |
| 5 | x:A, f:(AA), i,j:. f{i}{j}(x) = f{ij}(x) | [compose_iter_prod2] |
| cites the following: | ||
| 4 | x:A, f:(AA), i,j,k:. k = ij f{i}{j}(x) = f{k}(x) A | [compose_iter_prod] |