theorem mi2: :: FIELD_12:7

for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) ex E being b₁ -finite FieldExtension of F st
( deg (E,F) = deg p & p is_with_roots_in E )