theorem :: FIELD_1:21

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 . (Product (F ^ G)) = (h . (Product F)) * (h . (Product G))