let R be domRing; :: thesis: for B being non zero bag of the carrier of R

for p being Ppoly of R,B holds BRoots p = B

let B be non zero bag of the carrier of R; :: thesis: for p being Ppoly of R,B holds BRoots p = B

let p be Ppoly of R,B; :: thesis: BRoots p = B

set b = BRoots p;

for p being Ppoly of R,B holds BRoots p = B

let B be non zero bag of the carrier of R; :: thesis: for p being Ppoly of R,B holds BRoots p = B

let p be Ppoly of R,B; :: thesis: BRoots p = B

set b = BRoots p;

now :: thesis: for o being object st o in the carrier of R holds

(BRoots p) . o = B . o

hence
BRoots p = B
by PBOOLE:3; :: thesis: verum(BRoots p) . o = B . o

let o be object ; :: thesis: ( o in the carrier of R implies (BRoots p) . o = B . o )

assume o in the carrier of R ; :: thesis: (BRoots p) . o = B . o

then reconsider a = o as Element of the carrier of R ;

B . a = multiplicity (p,a) by dpp

.= (BRoots p) . a by UPROOTS:def 9 ;

hence (BRoots p) . o = B . o ; :: thesis: verum

end;assume o in the carrier of R ; :: thesis: (BRoots p) . o = B . o

then reconsider a = o as Element of the carrier of R ;

B . a = multiplicity (p,a) by dpp

.= (BRoots p) . a by UPROOTS:def 9 ;

hence (BRoots p) . o = B . o ; :: thesis: verum