let F be Field; :: thesis: for p being non zero Polynomial of F st ex a being Element of F st multiplicity (p,a) > 1 holds
card (Roots p) < card (BRoots p)
let p be non zero Polynomial of F; :: thesis: ( ex a being Element of F st multiplicity (p,a) > 1 implies card (Roots p) < card (BRoots p) )
H: card (Roots p) <= card (BRoots p) by RING_5:65;
assume ex a being Element of F st multiplicity (p,a) > 1 ; :: thesis: card (Roots p) < card (BRoots p)
then consider a being Element of F such that
B: multiplicity (p,a) > 1 ;
set n = multiplicity (p,a);
consider q being Polynomial of F such that
C: p = ((X- a) `^ (multiplicity (p,a))) *' q by mulzero1, RING_4:1;
reconsider q = q as non zero Polynomial of F by C;
D: card (BRoots p) = (card (BRoots ((X- a) `^ (multiplicity (p,a))))) + (card (BRoots q)) by C, RING_5:41;
J: 1 + (card (Roots q)) <= 1 + (card (BRoots q)) by RING_5:65, XREAL_1:6;

now :: thesis: not card (Roots p) = card (BRoots p)

assume E: card (Roots p) = card (BRoots p) ; :: thesis: contradiction
Roots ((X- a) `^ (multiplicity (p,a))) = {a} by B, Lm12b;
then F: card (Roots ((X- a) `^ (multiplicity (p,a)))) = 1 by CARD_2:42;
Roots p = (Roots ((X- a) `^ (multiplicity (p,a)))) \/ (Roots q) by C, UPROOTS:23;
then (card (BRoots ((X- a) `^ (multiplicity (p,a))))) + (card (BRoots q)) <= 1 + (card (Roots q)) by D, E, F, CARD_2:43;
then (card (BRoots ((X- a) `^ (multiplicity (p,a))))) + (card (BRoots q)) <= 1 + (card (BRoots q)) by J, XXREAL_0:2;
then card (BRoots ((X- a) `^ (multiplicity (p,a)))) <= 1 by XREAL_1:6;
hence contradiction by B, caBR; :: thesis: verum

end;

hence card (Roots p) < card (BRoots p) by H, XXREAL_0:1; :: thesis: verum