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)

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

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;

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

then card (Roots p) = 0
.= card (EmptyBag the carrier of R) by UPROOTS:11
.= card (BRoots p) by A, lemacf1 ;
hence card (Roots p) <= card (BRoots p) ; :: thesis: verum

end;

end;