theorem :: FIELD_1:29

for R being Ring
for S being b₁ -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) <= deg p by Lm2, XREAL_1:6;