theorem :: FIELD_1:25

for R being Ring
for S being b₁ -homomorphic Ring
for h being Homomorphism of R,S
for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p * q) = ((PolyHom h) . p) * ((PolyHom h) . q) by GROUP_6:def 6;