a,c,b:
, f:({a..b
}
).
Thm* a
c 
c<b 
{a..b}(f) = {a..c}(f)
cf(c){c+1..b}(f)a,c,b:, e:({a..b}).
Thm* a
c
Thm*
Thm* c<b
Thm*
Thm* (
i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i))| Rank | Theorem | Name |
| 5 | a,c,b:, f:({a..b}).
Thm* a c c<b {a..b}(f) = {a..c}(f)cf(c){c+1..b}(f) | [eval_factorization_split_pluck] |
| cites the following: | ||
| 4 | a,c,b:, e:({a..b}).
Thm* a c
Thm*
Thm* c<b Thm*
Thm* ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i)) | [mul_via_intseg_split_pluck] |