let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p is_a_root_of emb (p,p)
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: KrRoot p is_a_root_of emb (p,p)
A1: p - (0. (Polynom-Ring F)) in {p} -Ideal by IDEAL_1:66;
eval ((emb (p,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),p) by Th42
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(0. (Polynom-Ring F))) by A1, RING_1:6
.= 0. (KroneckerField (F,p)) by RING_1:def 6 ;
hence KrRoot p is_a_root_of emb (p,p) by POLYNOM5:def 7; :: thesis: verum