a,b:
, e:({a..b
}
).
Thm* a<b
(
i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))
e(b-1)f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* a<b
Thm*
Thm* (Iter(f;u) i:{a..b
}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1))| Rank | Theorem | Name |
| 2 | a,b:, e:({a..b}).
Thm* a<b ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))e(b-1) | [mul_via_intseg_split_last] |
| cites the following: | ||
| 1 | f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* a<b Thm*
Thm* (Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) | [iter_via_intseg_split_last] |