theorem Th43: :: FIELD_1:42

for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p is_a_root_of emb (p,p)