theorem x1000: :: FIELD_8:51

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
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)