a,b:
, e:({a..b
}
). b
a 
(
i:{a..b}. e(i)) = 1f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* b
a (Iter(f;u) i:{a..b}. e(i)) = u| Theorem | Name |
| a,b:, e:({a..b}). ba ( i:{a..b}. e(i)) = 1 | [mul_via_intseg_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] |