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) holds KrRoot (I,(g . p)) is_a_root_of (PolyHom (emb (F,I,g))) . 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) holds KrRoot (I,(g . p)) is_a_root_of (PolyHom (emb (F,I,g))) . p
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds KrRoot (I,(g . p)) is_a_root_of (PolyHom (emb (F,I,g))) . p
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: KrRoot (I,(g . p)) is_a_root_of (PolyHom (emb (F,I,g))) . p
set n = card (nonConstantPolys F);
set R = Polynom-Ring ((card (nonConstantPolys F)),F);
( rng g c= card (nonConstantPolys F) & dom g = nonConstantPolys F & p in nonConstantPolys F ) by FUNCT_2:def 1, RELAT_1:def 19;
then A0: g . p in card (nonConstantPolys F) by FUNCT_1:3;
reconsider q = Poly ((g . p),p) as Element of the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
A1: q in nonConstantPolys (g,F) ;
A3: nonConstantPolys (g,F) c= (nonConstantPolys (g,F)) -Ideal by IDEAL_1:def 14;
(nonConstantPolys (g,F)) -Ideal c= I by defideal;
then A2: q - (0. (Polynom-Ring ((card (nonConstantPolys F)),F))) in I by A1, A3;
eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,(g . p)))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),q) by A0, Kr2
.= Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(0. (Polynom-Ring ((card (nonConstantPolys F)),F)))) by A2, RING_1:6
.= 0. (KroneckerField (F,g,I)) by RING_1:def 6 ;
hence KrRoot (I,(g . p)) is_a_root_of (PolyHom (emb (F,I,g))) . p by POLYNOM5:def 7; :: thesis: verum