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 eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM 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 eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))
let f be Element of the carrier of (Polynom-Ring F); :: thesis: eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))
set LMf = Leading-Monomial f;
set LMfe = Leading-Monomial (emb (f,p));
set z = KrRoot p;
set E = KroneckerField (F,p);
set efp = emb (f,p);
set n = (len (emb (f,p))) -' 1;

per cases ( f = 0_. F or f <> 0_. F ) ;

suppose A1: f = 0_. F ; :: thesis: eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))

then emb (f,p) = 0_. (KroneckerField (F,p)) by Th23;
then Leading-Monomial (emb (f,p)) = 0_. (KroneckerField (F,p)) by POLYNOM4:13;
then A2: eval ((Leading-Monomial (emb (f,p))),(KrRoot p)) = 0. (KroneckerField (F,p)) by POLYNOM4:17
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(0. (Polynom-Ring F))) by RING_1:def 6 ;
0. (Polynom-Ring F) = 0_. F by POLYNOM3:def 10;
hence eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f)) by A1, A2, POLYNOM4:13; :: thesis: verum

end;

suppose f <> 0_. F ; :: thesis: eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))

then reconsider f1 = f as non zero Polynomial of F by UPROOTS:def 5;
reconsider fnF = (f . ((len (emb (f,p))) -' 1)) | F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider x = <%(0. F),(1. F)%> as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
A3: (emb (f,p)) . ((len (emb (f,p))) -' 1) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((f . ((len (emb (f,p))) -' 1)) | F)) by Th41;
A4: (power (KroneckerField (F,p))) . ((KrRoot p),((len (emb (f,p))) -' 1)) = (KrRoot p) |^ ((len (emb (f,p))) -' 1) by BINOM:def 2
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(x |^ ((len (emb (f,p))) -' 1))) by Th3 ;
set a = f . ((len (emb (f,p))) -' 1);
A5: deg f = deg (emb (f,p)) by Th32
.= (len (emb (f,p))) - 1 ;
then A6: (len (emb (f,p))) -' 1 = deg f1 by XREAL_0:def 2;
not LC f1 is zero ;
then A7: not f . ((len (emb (f,p))) -' 1) is zero by A5, RATFUNC1:def 6;
x |^ ((len (emb (f,p))) -' 1) = (power (Polynom-Ring F)) . (<%(0. F),(1. F)%>,((len (emb (f,p))) -' 1)) by BINOM:def 2
.= <%(0. F),(1. F)%> `^ ((len (emb (f,p))) -' 1) by POLYNOM5:def 3
.= anpoly ((1. F),((len (emb (f,p))) -' 1)) by Th13 ;
then A8: fnF * (x |^ ((len (emb (f,p))) -' 1)) = (anpoly ((f . ((len (emb (f,p))) -' 1)),0)) *' (anpoly ((1. F),((len (emb (f,p))) -' 1))) by POLYNOM3:def 10
.= anpoly (((f . ((len (emb (f,p))) -' 1)) * (1. F)),(0 + ((len (emb (f,p))) -' 1))) by A7, Th11
.= LM f by A6, Th12 ;
thus eval ((Leading-Monomial (emb (f,p))),(KrRoot p)) = ((emb (f,p)) . ((len (emb (f,p))) -' 1)) * ((power (KroneckerField (F,p))) . ((KrRoot p),((len (emb (f,p))) -' 1))) by POLYNOM4:22
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(Leading-Monomial f)) by A8, A3, A4, RING_1:14 ; :: thesis: verum

end;

end;