let L be domRing; :: thesis: for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q)
let p, q be non-zero Polynomial of L; :: thesis: BRoots (p *' q) = (BRoots p) + (BRoots q)

now

let i be set ; :: thesis: ( i in the carrier of L implies (BRoots (p *' q)) . i = ((BRoots p) + (BRoots q)) . i )
assume i in the carrier of L ; :: thesis: (BRoots (p *' q)) . i = ((BRoots p) + (BRoots q)) . i
then reconsider x = i as Element of L ;
thus (BRoots (p *' q)) . i = multiplicity (p *' q),x by Def9
.= (multiplicity p,x) + (multiplicity q,x) by Th57
.= ((BRoots p) . i) + (multiplicity q,x) by Def9
.= ((BRoots p) . i) + ((BRoots q) . i) by Def9
.= ((BRoots p) + (BRoots q)) . i by POLYNOM1:def 5 ; :: thesis: verum

end;

hence BRoots (p *' q) = (BRoots p) + (BRoots q) by PBOOLE:3; :: thesis: verum