a,b,c:
. (a
b)
c = acbca,b:
, f,g:({a..b
}
).
Thm* (
i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i))| Rank | Theorem | Name |
| 4 | a,b,c:. (ab)c = acbc | [exp_reduce1] |
| cites the following: | ||
| 3 | a,b:, f,g:({a..b}).
Thm* ( i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i)) | [mul_via_intseg_factors] |