theorem TH39: :: FIELD_11:39

for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for a being Element of F holds (emb (F,I,g)) . a = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(a | ((card (nonConstantPolys F)),F)))