let R be domRing; :: thesis: for p being non zero Polynomial of R holds card (Roots p) <= card (BRoots p)

let p be non zero Polynomial of R; :: thesis: card (Roots p) <= card (BRoots p)

let p be non zero Polynomial of R; :: thesis: card (Roots p) <= card (BRoots p)

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

end;

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

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

A: ( p1 = q *' r & Roots q = Roots p1 ) by acf;

deg q = card (BRoots q) by lemacf5

.= card (BRoots p1) by pf2 ;

hence card (Roots p) <= card (BRoots p) by A, degpoly; :: thesis: verum

end;consider q being Ppoly of R, BRoots p1, r being non with_roots Polynomial of R such that

A: ( p1 = q *' r & Roots q = Roots p1 ) by acf;

deg q = card (BRoots q) by lemacf5

.= card (BRoots p1) by pf2 ;

hence card (Roots p) <= card (BRoots p) by A, degpoly; :: thesis: verum