let R be domRing; :: thesis: for p being non constant Polynomial of R holds
( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q )
let p be non constant Polynomial of R; :: thesis: ( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q )

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

suppose p is with_roots ; :: thesis: ( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q )

then reconsider p1 = p as non zero with_roots Polynomial of R ;
consider q being Ppoly of R, BRoots p1, r being non with_roots Polynomial of R such that
H: ( p1 = q *' r & Roots q = Roots p1 ) by acf;
reconsider r1 = r as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

A: now :: thesis: ( card (BRoots p) = deg p implies ex a being Element of R ex q being Ppoly of R st p = a * q )

assume A1: card (BRoots p) = deg p ; :: thesis: ex a being Element of R ex q being Ppoly of R st p = a * q
( r <> 0_. R & q <> 0_. R ) ;
then deg p = (deg q) + (deg r) by H, HURWITZ:23
.= (card (BRoots q)) + (deg r) by lemacf5
.= (deg p) + (deg r) by A1, pf2 ;
then r1 is constant ;
then consider a being Element of R such that
B: r1 = a | R by RING_4:20;
p = q *' (a * (1_. R)) by H, B, RING_4:16
.= a * (q *' (1_. R)) by RATFUNC1:6
.= a * q ;
hence ex a being Element of R ex q being Ppoly of R st p = a * q ; :: thesis: verum

end;

now :: thesis: ( ex a being Element of R ex q being Ppoly of R st p = a * q implies deg p = card (BRoots p) )

assume ex a being Element of R ex q being Ppoly of R st p = a * q ; :: thesis: deg p = card (BRoots p)
then consider a being Element of R, q being Ppoly of R such that
A1: p = a * q ;
set B = BRoots q;
reconsider q = q as Ppoly of R, BRoots q by lll;
p <> 0_. R ;
then A3: not a is zero by A1, POLYNOM5:26;
hence deg p = deg q by A1, Th25
.= card (BRoots q) by lemacf5
.= card (BRoots p) by A1, A3, llll ;
:: thesis: verum

end;

hence ( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q ) by A; :: thesis: verum

end;

suppose A: not p is with_roots ; :: thesis: ( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q )

then reconsider p1 = p as non zero non with_roots Polynomial of R ;
card (BRoots p) = card (EmptyBag the carrier of R) by A, lemacf1
.= 0 by UPROOTS:11 ;
hence ( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q ) by A, RATFUNC1:def 2; :: thesis: verum

end;

end;