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 constant Element of the carrier of (Polynom-Ring F)
for n being Ordinal holds eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,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 constant Element of the carrier of (Polynom-Ring F)
for n being Ordinal holds eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p)))
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ; :: thesis: for p being constant Element of the carrier of (Polynom-Ring F)
for n being Ordinal holds eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p)))
let p be constant Element of the carrier of (Polynom-Ring F); :: thesis: for n being Ordinal holds eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p)))
let n be Ordinal; :: thesis: eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p)))
set E = KroneckerField (F,g,I);
set u = KrRoot (I,n);
set m = card (nonConstantPolys F);
reconsider q = (PolyHom (emb (F,I,g))) . p as Element of the carrier of (Polynom-Ring (KroneckerField (F,g,I))) ;
( deg q = deg p & deg p <= 0 ) by FIELD_1:31, RING_4:def 4;
then reconsider q = q as constant Element of the carrier of (Polynom-Ring (KroneckerField (F,g,I))) by RING_4:def 4;
consider c being Element of F such that
H0: p = c | F by RING_4:20;
reconsider r = Poly (n,(c | F)) as Element of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
set h = emb (F,I,g);
q = ((emb (F,I,g)) . c) | (KroneckerField (F,g,I)) by H0, FIELD_8:13;
hence eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = (emb (F,I,g)) . c by RING_5:8
.= Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(c | ((card (nonConstantPolys F)),F))) by TH39
.= Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p))) by H0, lemKr3 ;
:: thesis: verum