theorem Th23: :: E_TRANS1:23

for R being domRing
for h being Function of R,R
for s being FinSequence of the carrier of R st h is additive holds
h . (Sum s) = Sum (h * s)