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)

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

hence
BRoots (p *' q) = (BRoots p) + (BRoots q)
by PBOOLE:3; :: thesis: verum(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;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