theorem :: FIELD_5:19

for F being strict Field
for p being linear Element of the carrier of (Polynom-Ring F) holds embField (canHomP p) = F