theorem ft1: :: FIELD_7:36

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds
( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) )