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 ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),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 ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)
let f be Element of the carrier of (Polynom-Ring F); :: thesis: eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)
set z = KrRoot p;
set E = KroneckerField (F,p);
set h = canHom (emb p);
defpred S₁[ Nat] means for f being Element of the carrier of (Polynom-Ring F) st len f = $1 holds
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f);

A1: now :: thesis: for f being Element of the carrier of (Polynom-Ring F) st len f = 0 holds
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)

let f be Element of the carrier of (Polynom-Ring F); :: thesis: ( len f = 0 implies eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f) )
assume len f = 0 ; :: thesis: eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)
then f = 0_. F by POLYNOM4:5;
then A2: f = 0. (Polynom-Ring F) by POLYNOM3:def 10;
0_. (KroneckerField (F,p)) = 0. (Polynom-Ring (KroneckerField (F,p))) by POLYNOM3:def 10
.= emb (f,p) by A2, RING_2:6 ;
hence eval ((emb (f,p)),(KrRoot p)) = 0. (KroneckerField (F,p)) by POLYNOM4:17
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f) by A2, RING_1:def 6 ;
:: thesis: verum

end;

A3: now :: thesis: for k being Nat st ( for m being Nat st m < k holds
S₁[m] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for m being Nat st m < k holds
S₁[m] ) implies S₁[k] )
assume A4: for m being Nat st m < k holds
S₁[m] ; :: thesis: S₁[k]

now :: thesis: for f being Element of the carrier of (Polynom-Ring F) st len f = k holds
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)

let f be Element of the carrier of (Polynom-Ring F); :: thesis: ( len f = k implies eval ((emb (b₁,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b₁) )
assume A5: len f = k ; :: thesis: eval ((emb (b₁,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b₁)

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: eval ((emb (b₁,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b₁)

hence eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f) by A5, A1; :: thesis: verum

end;

suppose k > 0 ; :: thesis: eval ((emb (b₁,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b₁)

then consider q being Polynomial of F such that
A6: ( len q < len f & f = q + (Leading-Monomial f) & ( for n being Element of NAT st n < (len f) - 1 holds
q . n = f . n ) ) by A5, POLYNOM4:16;
reconsider g = q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider LMf = LM f as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider r1 = emb (LMf,p), r2 = emb (g,p) as Polynomial of (KroneckerField (F,p)) ;
A7: emb ((LMf + g),p) = (emb (LMf,p)) + (emb (g,p)) by VECTSP_1:def 20
.= r1 + r2 by POLYNOM3:def 10 ;
Leading-Monomial (emb (f,p)) = emb (LMf,p) by Th33;
then A8: eval ((emb (LMf,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),LMf) by Lm5;
A9: eval ((emb (g,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),g) by A6, A5, A4;
A10: (eval ((emb (LMf,p)),(KrRoot p))) + (eval ((emb (g,p)),(KrRoot p))) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LMf + g)) by A9, A8, RING_1:13
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f) by A6, POLYNOM3:def 10 ;
thus eval ((emb (f,p)),(KrRoot p)) = eval ((r1 + r2),(KrRoot p)) by A7, A6, POLYNOM3:def 10
.= Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f) by A10, POLYNOM4:19 ; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

A11: for k being Nat holds S₁[k] from NAT_1:sch 4(A3);
ex n being Nat st len f = n ;
hence eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f) by A11; :: thesis: verum