let F be Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) holds
( ex a being Element of F st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) is with_roots )
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( ex a being Element of F st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) is with_roots )
set g = p gcd ((Deriv F) . p);

A: now :: thesis: ( ex a being Element of F st multiplicity (p,a) > 1 implies p gcd ((Deriv F) . p) is with_roots )

assume ex a being Element of F st multiplicity (p,a) > 1 ; :: thesis: p gcd ((Deriv F) . p) is with_roots
then consider a being Element of F such that
A1: multiplicity (p,a) > 1 ;
A2: a is_a_root_of p by A1, UPROOTS:52;
eval (p,a) = 0. F by POLYNOM5:def 7, A1, UPROOTS:52;
then A3: rpoly (1,a) divides p by RING_5:11;
eval (((Deriv F) . p),a) = 0. F by A1, A2, multi4;
then rpoly (1,a) divides (Deriv F) . p by RING_5:11;
then eval ((p gcd ((Deriv F) . p)),a) = 0. F by A3, RING_4:52, RING_5:11;
hence p gcd ((Deriv F) . p) is with_roots by POLYNOM5:def 7; :: thesis: verum

end;

now :: thesis: ( p gcd ((Deriv F) . p) is with_roots implies ex a being Element of F st multiplicity (p,a) > 1 )

assume p gcd ((Deriv F) . p) is with_roots ; :: thesis: ex a being Element of F st multiplicity (p,a) > 1
then consider a being Element of F such that
B7: a is_a_root_of p gcd ((Deriv F) . p) ;
a is_a_root_of p by B7, mm1, RING_4:52;
then B4: ( multiplicity (p,a) > 1 iff eval (((Deriv F) . p),a) = 0. F ) by multi4;
a is_a_root_of (Deriv F) . p by B7, mm1, RING_4:52;
hence ex a being Element of F st multiplicity (p,a) > 1 by B4; :: thesis: verum

end;

hence ( ex a being Element of F st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) is with_roots ) by A; :: thesis: verum