theorem :: FIELD_1:28

for R being domRing
for S being b₁ -homomorphic domRing
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))