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 a being Element of F holds (emb (F,I,g)) . a = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(a | ((card (nonConstantPolys F)),F)))
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)); :: thesis: for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for a being Element of F holds (emb (F,I,g)) . a = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(a | ((card (nonConstantPolys F)),F)))
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ; :: thesis: for a being Element of F holds (emb (F,I,g)) . a = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(a | ((card (nonConstantPolys F)),F)))
let a be Element of F; :: thesis: (emb (F,I,g)) . a = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(a | ((card (nonConstantPolys F)),F)))
set n = card (nonConstantPolys F);
set R = Polynom-Ring ((card (nonConstantPolys F)),F);
reconsider pa = a | ((card (nonConstantPolys F)),F) as Element of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
dom (canHom ((card (nonConstantPolys F)),F)) = the carrier of F by FUNCT_2:def 1;
then (emb (F,I,g)) . a = (canHom I) . ((canHom ((card (nonConstantPolys F)),F)) . a) by FUNCT_1:13
.= (canHom I) . pa by defcanhom
.= Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),pa) by RING_2:def 5 ;
hence (emb (F,I,g)) . a = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(a | ((card (nonConstantPolys F)),F))) ; :: thesis: verum