theorem Th40: :: FIELD_1:39

for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for a being Element of F holds (emb p) . a = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F))