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

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