:: deftheorem defcanhom defines canHom RING_4:def 6 :
for R being Ring
for b₂ being Function of R,(Polynom-Ring R) holds
( b₂ = canHom R iff for x being Element of R holds b₂ . x = x | R );