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;
now :: thesis: for o being object st o in the carrier of R holds
(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;
hence BRoots p = B by PBOOLE:3; :: thesis: verum