let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )
let a be F -algebraic Element of E; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )
set m = MinPoly (a,F);
X: F is Subring of E by FIELD_4:def 1;
Y: a is_integral_over F by alg1;
then Z: ( MinPoly (a,F) <> 0_. F & {(MinPoly (a,F))} -Ideal = Ann_Poly (a,F) & MinPoly (a,F) = NormPolynomial (MinPoly (a,F)) ) by X, ALGNUM_1:def 9;

now :: thesis: ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal implies p = MinPoly (a,F) )

assume A0: ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) ; :: thesis: p = MinPoly (a,F)
then A1: p <> 0_. F ;
A2: {p} -Ideal = Ann_Poly (a,F) by A0, alg0;
p = NormPolynomial p by A0, RING_4:24;
hence p = MinPoly (a,F) by X, Y, A1, A2, ALGNUM_1:def 9; :: thesis: verum

end;

hence ( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) ) by Z, alg0; :: thesis: verum