let R be domRing; :: thesis: for B1, B2 being non zero bag of the carrier of R
for p being Ppoly of R,B1
for q being Ppoly of R,B2 holds p *' q is Ppoly of R,B1 + B2
let B1, B2 be non zero bag of the carrier of R; :: thesis: for p being Ppoly of R,B1
for q being Ppoly of R,B2 holds p *' q is Ppoly of R,B1 + B2
set B = B1 + B2;
let p be Ppoly of R,B1; :: thesis: for q being Ppoly of R,B2 holds p *' q is Ppoly of R,B1 + B2
let q be Ppoly of R,B2; :: thesis: p *' q is Ppoly of R,B1 + B2
reconsider r = p *' q as Ppoly of R by lemppoly3;
( p <> 0_. R & q <> 0_. R ) ;
then A: deg r = (deg p) + (deg q) by HURWITZ:23
.= (card (BRoots p)) + (deg q) by lemacf5
.= (card B1) + (deg q) by pf2
.= (card B1) + (card (BRoots q)) by lemacf5
.= (card B1) + (card B2) by pf2
.= card (B1 + B2) by UPROOTS:15 ;

now :: thesis: for c being Element of R holds multiplicity (r,c) = (B1 + B2) . c

let c be Element of R; :: thesis: multiplicity (r,c) = (B1 + B2) . c
thus multiplicity (r,c) = (multiplicity (p,c)) + (multiplicity (q,c)) by UPROOTS:55
.= ((BRoots p) . c) + (multiplicity (q,c)) by UPROOTS:def 9
.= (B1 . c) + (multiplicity (q,c)) by pf2
.= (B1 . c) + ((BRoots q) . c) by UPROOTS:def 9
.= (B1 . c) + (B2 . c) by pf2
.= (B1 + B2) . c by PRE_POLY:def 5 ; :: thesis: verum

end;

hence p *' q is Ppoly of R,B1 + B2 by A, dpp; :: thesis: verum