let F be Field; :: thesis: 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))
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of F holds (emb p) . a = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F))
let a be Element of F; :: thesis: (emb p) . a = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F))
reconsider pa = a | F as Element of (Polynom-Ring F) by POLYNOM3:def 10;
dom (canHom F) = the carrier of F by FUNCT_2:def 1;
hence (emb p) . a = (canHom ({p} -Ideal)) . ((canHom F) . a) by FUNCT_1:13
.= (canHom ({p} -Ideal)) . pa by RING_4:def 6
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F)) by RING_2:def 5 ;
:: thesis: verum