let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
( ex a being Element of E st multiplicity (p,a) > 1 iff (Deriv F) . p = 0_. F )
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F st p splits_in E holds
( ex a being Element of E st multiplicity (p,a) > 1 iff (Deriv F) . p = 0_. F )
let E be FieldExtension of F; :: thesis: ( p splits_in E implies ( ex a being Element of E st multiplicity (p,a) > 1 iff (Deriv F) . p = 0_. F ) )
assume AS: p splits_in E ; :: thesis: ( ex a being Element of E st multiplicity (p,a) > 1 iff (Deriv F) . p = 0_. F )
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring E) ;
deg p1 = deg p by FIELD_4:20;
then reconsider p1 = p1 as non zero Element of the carrier of (Polynom-Ring E) by RATFUNC1:def 2, RING_4:def 4;
set g = p gcd ((Deriv F) . p);
H: p gcd ((Deriv F) . p) is monic Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

A: now :: thesis: ( ex a being Element of E st multiplicity (p,a) > 1 implies (Deriv F) . p = 0_. F )

assume A2: ex a being Element of E st multiplicity (p,a) > 1 ; :: thesis: (Deriv F) . p = 0_. F
( p gcd ((Deriv F) . p) = 1_. F or p gcd ((Deriv F) . p) = NormPolynomial p ) by RING_4:52, H, lemir;
then A4: deg (p gcd ((Deriv F) . p)) = deg p by AS, A2, lemsep3, REALALG3:11;

now :: thesis: not (Deriv F) . p <> 0_. F

assume (Deriv F) . p <> 0_. F ; :: thesis: contradiction
then not (Deriv F) . p is zero by UPROOTS:def 5;
then deg (p gcd ((Deriv F) . p)) <= deg ((Deriv F) . p) by RING_4:52, RING_5:13;
hence contradiction by A4, FIELD_14:64; :: thesis: verum

end;

hence (Deriv F) . p = 0_. F ; :: thesis: verum

end;

now :: thesis: ( (Deriv F) . p = 0_. F implies ex a being Element of E st multiplicity (p,a) > 1 )

assume (Deriv F) . p = 0_. F ; :: thesis: ex a being Element of E st multiplicity (p,a) > 1
then B1: p gcd ((Deriv F) . p) = NormPolynomial p by FIELD_14:46;
deg (NormPolynomial p) = deg p by REALALG3:11;
then p gcd ((Deriv F) . p) <> 1_. F by B1, RATFUNC1:def 2, RING_4:def 4;
then consider a being Element of E such that
B2: multiplicity (p,a) > 1 by AS, lemsep3;
thus ex a being Element of E st multiplicity (p,a) > 1 by B2; :: thesis: verum

end;

hence ( ex a being Element of E st multiplicity (p,a) > 1 iff (Deriv F) . p = 0_. F ) by A; :: thesis: verum