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 n being Element of NAT holds ((PolyHom (emb (F,I,g))) . p) . n = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . n) | ((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 p being Element of the carrier of (Polynom-Ring F)
for n being Element of NAT holds ((PolyHom (emb (F,I,g))) . p) . n = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . n) | ((card (nonConstantPolys F)),F)))
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for n being Element of NAT holds ((PolyHom (emb (F,I,g))) . p) . n = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . n) | ((card (nonConstantPolys F)),F)))
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for n being Element of NAT holds ((PolyHom (emb (F,I,g))) . p) . n = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . n) | ((card (nonConstantPolys F)),F)))
let m be Nat; :: thesis: ( m is Element of NAT implies ((PolyHom (emb (F,I,g))) . p) . m = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . m) | ((card (nonConstantPolys F)),F))) )
set n = card (nonConstantPolys F);
set R = Polynom-Ring ((card (nonConstantPolys F)),F);
((PolyHom (emb (F,I,g))) . p) . m = (emb (F,I,g)) . (p . m) by FIELD_1:def 2
.= Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . m) | ((card (nonConstantPolys F)),F))) by TH39 ;
hence ( m is Element of NAT implies ((PolyHom (emb (F,I,g))) . p) . m = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . m) | ((card (nonConstantPolys F)),F))) ) ; :: thesis: verum