a,b:
, f:({a..b
}
). b
a 
{a..b}(f) = 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:, f:({a..b}). ba {a..b}(f) = 1 | [eval_factorization_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] |