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 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 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 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 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 m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p))) )
assume A0: m in card (nonConstantPolys F) ; :: thesis: eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p)))

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

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

hence eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p))) by Kr2a; :: thesis: verum

end;

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

hence eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p))) by A0, Kr3; :: thesis: verum

end;

end;