theorem polyd1: :: FIELD_5:20

for F being Field
for p being linear Element of the carrier of (Polynom-Ring F) holds
( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )