m,k:
. m = 0 
k!m = 1 f:(A
AA), u:A, a,b:
, e:({a..b
}A).
Thm* b
a (Iter(f;u) i:{a..b}. e(i)) = u| Theorem | Name |
| m,k:. m = 0 k!m = 1 | [factorial_tail_via_iter_null] |
| cites the following: | |
| f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* b a (Iter(f;u) i:{a..b}. e(i)) = u | [iter_via_intseg_null] |