let F be Field; :: thesis: for p being non zero Polynomial of F holds
( card (Roots p) < card (BRoots p) iff ex a being Element of F st multiplicity (p,a) > 1 )
let p be non zero Polynomial of F; :: thesis: ( card (Roots p) < card (BRoots p) iff ex a being Element of F st multiplicity (p,a) > 1 )

now :: thesis: ( ( for a being Element of F holds not multiplicity (p,a) > 1 ) implies card (BRoots p) = card (Roots p) )

assume AS: for a being Element of F holds not multiplicity (p,a) > 1 ; :: thesis: card (BRoots p) = card (Roots p)

per cases ( not p is with_roots or p is with_roots ) ;

suppose not p is with_roots ; :: thesis: card (BRoots p) = card (Roots p)

then A: Roots p = {} ;
then support (BRoots p) = {} by UPROOTS:def 9;
hence card (BRoots p) = card (Roots p) by A, RING_5:23; :: thesis: verum

end;

suppose S: p is with_roots ; :: thesis: card (Roots p) = card (BRoots p)

defpred S₁[ Nat] means for p being non zero with_roots Polynomial of F st deg p = $1 & ( for a being Element of F holds not multiplicity (p,a) > 1 ) holds
card (Roots p) = card (BRoots p);

IS: now :: thesis: for k being Nat st 1 <= k & ( for n being Nat st 1 <= n & n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( 1 <= k & ( for n being Nat st 1 <= n & n < k holds
S₁[n] ) implies S₁[k] )
assume IV: ( 1 <= k & ( for n being Nat st 1 <= n & n < k holds
S₁[n] ) ) ; :: thesis: S₁[k]

now :: thesis: for p being non zero with_roots Polynomial of F st deg p = k & ( for a being Element of F holds not multiplicity (p,a) > 1 ) holds
card (Roots p) = card (BRoots p)

let p be non zero with_roots Polynomial of F; :: thesis: ( deg p = k & ( for a being Element of F holds not multiplicity (p,a) > 1 ) implies card (Roots b₁) = card (BRoots b₁) )
assume A: ( deg p = k & ( for a being Element of F holds not multiplicity (p,a) > 1 ) ) ; :: thesis: card (Roots b₁) = card (BRoots b₁)
consider q being Ppoly of F, BRoots p, r being non with_roots Polynomial of F such that
B: ( p = q *' r & Roots q = Roots p ) by RING_5:64;
reconsider r = r as non zero non with_roots Polynomial of F ;

F: now :: thesis: for a being Element of F holds not multiplicity (q,a) > 1

assume ex a being Element of F st multiplicity (q,a) > 1 ; :: thesis: contradiction
then consider a being Element of F such that
D: multiplicity (q,a) > 1 ;
multiplicity (p,a) = (multiplicity (q,a)) + (multiplicity (r,a)) by B, UPROOTS:55;
then multiplicity (p,a) >= multiplicity (q,a) by NAT_1:11;
then multiplicity (p,a) > 1 by D, XXREAL_0:2;
hence contradiction by A; :: thesis: verum

end;

per cases ( r is constant or not r is constant ) ;

suppose D0: r is constant ; :: thesis: card (Roots b₁) = card (BRoots b₁)

reconsider r1 = r as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg r <= 0 by D0, RATFUNC1:def 2;
then reconsider r1 = r1 as constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4;
consider b being Element of F such that
D1: r1 = b | F by RING_4:20;
b <> 0. F by D1;
then reconsider b = b as non zero Element of F by STRUCT_0:def 12;
r = b * (1_. F) by D1, RING_4:16;
then p = b * ((1_. F) *' q) by B, RING_4:10
.= b * q ;
then C1: BRoots p = BRoots q by RING_5:37;
C0: deg q = card (BRoots q) by RING_5:56;

now :: thesis: for a being Element of F st a is_a_root_of q holds
multiplicity (q,a) = 1

let a be Element of F; :: thesis: ( a is_a_root_of q implies multiplicity (q,a) = 1 )
assume a is_a_root_of q ; :: thesis: multiplicity (q,a) = 1
then ( multiplicity (q,a) >= 1 & multiplicity (q,a) <= 1 ) by F, UPROOTS:52;
hence multiplicity (q,a) = 1 by XXREAL_0:1; :: thesis: verum

end;

then q is Ppoly of F,(Roots q) by FIELD_14:30;
hence card (Roots p) = card (BRoots p) by B, C1, C0, RING_5:60; :: thesis: verum

end;

suppose not r is constant ; :: thesis: card (Roots b₁) = card (BRoots b₁)

then C0: deg r >= 0 + 1 by INT_1:7, RATFUNC1:def 2;
C1: 0 + 1 <= deg q by INT_1:7, RATFUNC1:def 2;
( q <> 0_. F & r <> 0_. F ) ;
then C3: deg p = (deg q) + (deg r) by B, HURWITZ:23;

D: now :: thesis: not deg q >= k

assume deg q >= k ; :: thesis: contradiction
then ( k >= k + 1 & k <= k + 1 ) by A, C0, C3, NAT_1:11, XREAL_1:7;
then k = k + 1 by XXREAL_0:1;
hence contradiction ; :: thesis: verum

end;

BRoots r = EmptyBag the carrier of F by RING_5:38;
then support (BRoots r) = {} ;
then card (BRoots r) = 0 by RING_5:23;
then card (BRoots p) = (card (BRoots q)) + 0 by B, RING_5:41;
hence card (Roots p) = card (BRoots p) by D, B, F, C1, IV; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

I: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 9(IS);
deg p >= 0 + 1 by S, INT_1:7, RATFUNC1:def 2;
hence card (Roots p) = card (BRoots p) by S, AS, I; :: thesis: verum

end;

end;

end;

hence ( card (Roots p) < card (BRoots p) iff ex a being Element of F st multiplicity (p,a) > 1 ) by ABC1; :: thesis: verum