theorem :: FIELD_8:54

for F being Field
for E being FieldExtension of F
for a, b being b₁ -algebraic Element of E holds
( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )