let n be Nat; :: thesis: 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))
let F be Field; :: thesis: 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))
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: 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))
let f be Element of the carrier of (Polynom-Ring F); :: thesis: (emb (f,p)) . n = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((f . n) | F))
thus (emb (f,p)) . n = (emb p) . (f . n) by Def2
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((f . n) | F)) by Th40 ; :: thesis: verum