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 ;

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

hence
p *' q is Ppoly of R,B1 + B2
by A, dpp; :: thesis: verumlet 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;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