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 )

( 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 )
;

end;

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;

end;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;( 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

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

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: verumassume
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;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

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;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