let R be domRing; :: thesis: for p being non zero non with_roots Polynomial of R holds BRoots p = EmptyBag the carrier of R
let p be non zero non with_roots Polynomial of R; :: thesis: BRoots p = EmptyBag the carrier of R
Roots p is empty ;
then support (BRoots p) = {} by UPROOTS:def 9;
hence BRoots p = EmptyBag the carrier of R by PRE_POLY:81; :: thesis: verum