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