theorem Kr2: :: FIELD_11:41

for F being Field
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)))