theorem Kr1: :: FIELD_11:42

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 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