theorem :: FIELD_1:24

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 VECTSP_1:def 20;