theorem Th42: :: FIELD_1:41

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 eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)