theorem Th41: :: FIELD_1:40

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