:: deftheorem Def2 defines PolyHom FIELD_1:def 2 :
for R being Ring
for S being b₁ -homomorphic Ring
for h being additive Function of R,S
for b₄ being Function of (Polynom-Ring R),(Polynom-Ring S) holds
( b₄ = PolyHom h iff for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b₄ . f) . i = h . (f . i) );