a,b:
, f:({a..b
}
). b
a 
{a..b}(f) = {a..a}(f)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))| Rank | Theorem | Name |
| 2 | a,b:, f:({a..b}). ba {a..b}(f) = {a..a}(f) | [eval_factorization_nullnorm] |
| cites the following: | ||
| 1 | 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] |