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 :: thesis: for i being object st i in the carrier of L holds
(BRoots (p *' q)) . i = ((BRoots p) + (BRoots q)) . i

let i be object ; :: 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 Def8
.= (multiplicity (p,x)) + (multiplicity (q,x)) by Th52
.= ((BRoots p) . i) + (multiplicity (q,x)) by Def8
.= ((BRoots p) . i) + ((BRoots q) . i) by Def8
.= ((BRoots p) + (BRoots q)) . i by PRE_POLY:def 5 ; :: thesis: verum

end;

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