for F1 being Field
for F2 being b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being b₁ -algebraic Element of E1
for b being b₂ -algebraic Element of E2 st Ext_eval (((PolyHom h) . (MinPoly (a,F1))),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)