a,c,b:
, f:({a..b
}
).
Thm* a
c 
cb 
{a..b}(f) = {a..c}(f)
{c..b}(f)a,c,b:, e:({a..b}).
Thm* a
c
Thm*
Thm* c
b ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))| Rank | Theorem | Name |
| 4 | a,c,b:, f:({a..b}).
Thm* a c cb {a..b}(f) = {a..c}(f){c..b}(f) | [eval_factorization_split_mid] |
| cites the following: | ||
| 3 | a,c,b:, e:({a..b}).
Thm* a c
Thm*
Thm* c b ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i)) | [mul_via_intseg_split_mid] |