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