:: deftheorem defch defines canHomP FIELD_5:def 2 :
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for b₃ being Function of F,(Polynom-Ring p) holds
( b₃ = canHomP p iff for a being Element of F holds b₃ . a = a | F );