let F be Field; :: thesis: for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p)))
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)); :: thesis: for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p)))
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p)))
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p)))
let n be Ordinal; :: thesis: ( n in card (nonConstantPolys F) implies eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p))) )
assume A0: n in card (nonConstantPolys F) ; :: thesis: eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p)))
set m = card (nonConstantPolys F);
set E = KroneckerField (F,g,I);
set h = canHom (emb (F,I,g));
defpred S₁[ Nat] means for f being non constant Element of the carrier of (Polynom-Ring F) st len f = $1 holds
eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f)));

A1: now :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) st len f = 0 holds
eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f)))

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( len f = 0 implies eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f))) )
assume B: len f = 0 ; :: thesis: eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f)))
deg f = (len f) - 1 by HURWITZ:def 2;
hence eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f))) by B; :: 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 IV: for m being Nat st m < k holds
S₁[m] ; :: thesis: S₁[k]

now :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) st len f = k holds
eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f)))

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( len f = k implies eval (((PolyHom (emb (F,I,g))) . b₁),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,b₁))) )
assume A5: len f = k ; :: thesis: eval (((PolyHom (emb (F,I,g))) . b₁),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,b₁)))

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

suppose k = 0 ; :: thesis: eval (((PolyHom (emb (F,I,g))) . b₁),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,b₁)))

hence eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f))) by A5, A1; :: thesis: verum

end;

suppose k > 0 ; :: thesis: eval (((PolyHom (emb (F,I,g))) . b₁),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,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 q = 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 = (PolyHom (emb (F,I,g))) . LMf, r2 = (PolyHom (emb (F,I,g))) . q, f1 = (PolyHom (emb (F,I,g))) . f as Polynomial of (KroneckerField (F,g,I)) ;
A7: (PolyHom (emb (F,I,g))) . f = (PolyHom (emb (F,I,g))) . (LMf + q) by A6, POLYNOM3:def 10
.= ((PolyHom (emb (F,I,g))) . LMf) + ((PolyHom (emb (F,I,g))) . q) by VECTSP_1:def 20
.= r1 + r2 by POLYNOM3:def 10 ;
A14: LM ((PolyHom (emb (F,I,g))) . f) = (PolyHom (emb (F,I,g))) . LMf by FIELD_1:32;
A8: eval ((LM ((PolyHom (emb (F,I,g))) . f)),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (n,f)))) by A0, lemKr2;
A11: Poly (n,f) = (Poly (n,(LM f))) + (Poly (n,q)) by A6, Th14
.= (LM (Poly (n,f))) + (Poly (n,q)) by A0, Th14y ;
( LM (Poly (n,f)) is Element of (Polynom-Ring ((card (nonConstantPolys F)),F)) & Poly (n,q) is Element of (Polynom-Ring ((card (nonConstantPolys F)),F)) ) by POLYNOM1:def 11;
then reconsider a1 = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (n,f)))), a2 = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,q))) as Element of (KroneckerField (F,g,I)) by RING_1:12;
reconsider u = Poly (n,f), u1 = LM (Poly (n,f)), u2 = Poly (n,q) as Element of the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
A16: a1 + a2 = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(u1 + u2)) by RING_1:13;
A18: u1 + u2 = Poly (n,f) by A11, POLYNOM1:def 11;

per cases ( not q is constant or q is constant ) ;

suppose not q is constant ; :: thesis: eval (((PolyHom (emb (F,I,g))) . b₁),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,b₁)))

then eval (((PolyHom (emb (F,I,g))) . q),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,q))) by A5, A6, IV;
hence eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f))) by A8, A16, A18, A14, A7, POLYNOM4:19; :: thesis: verum

end;

suppose q is constant ; :: thesis: eval (((PolyHom (emb (F,I,g))) . b₁),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,b₁)))

then eval (((PolyHom (emb (F,I,g))) . q),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,q))) by Kr2a;
hence eval (((PolyHom (emb (F,I,g))) . f),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,f))) by A8, A16, A18, A14, A7, POLYNOM4:19; :: thesis: verum

end;

end;

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 p = n ;
hence eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p))) by A11; :: thesis: verum