let R be domRing; :: thesis: for p being non constant Polynomial of R holds
( card () = 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 () = 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 () = 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 () by POLYNOM3:def 10;
A: now :: thesis: ( card () = deg p implies ex a being Element of R ex q being Ppoly of R st p = a * q )
assume A1: card () = 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
.= (card ()) + (deg r) by lemacf5
.= (deg p) + (deg r) by ;
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
.= 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 () )
assume ex a being Element of R ex q being Ppoly of R st p = a * q ; :: thesis: deg p = card ()
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 ;
hence deg p = deg q by
.= card () by lemacf5
.= card () by A1, A3, llll ;
:: thesis: verum
end;
hence ( card () = 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 () = 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 () = card (EmptyBag the carrier of R) by
.= 0 by UPROOTS:11 ;
hence ( card () = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q ) by ; :: thesis: verum
end;
end;