theorem :: FIELD_8:54
for F being Field
for E being FieldExtension of F
for a, b being b1 -algebraic Element of E holds
( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )