let L be domRing; :: thesis: for p being non-zero Polynomial of L st len p = 1 holds
degree (BRoots p) = 0
let p be non-zero Polynomial of L; :: thesis: ( len p = 1 implies degree (BRoots p) = 0 )
assume len p = 1 ; :: thesis: degree (BRoots p) = 0
then Roots p = {} by Th48;
then support (BRoots p) = {} by Def9;
then BRoots p = EmptyBag the carrier of L by BAGORDER:19;
hence degree (BRoots p) = 0 by Th13; :: thesis: verum