for R being Ring
for S being b₁ -homomorphic Ring
for h being Homomorphism of R,S
for F, G being FinSequence of R holds h . (Sum (F ^ G)) = (h . (Sum F)) + (h . (Sum G))