theorem Th17: :: FIELD_1:16

for R being Ring
for S being b₁ -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Sum (F ^ <*a*>)) = (h . (Sum F)) + (h . a)