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 Th43;
then support (BRoots p) = {} by Def8;
then BRoots p = EmptyBag the carrier of L by PRE_POLY:81;
hence degree (BRoots p) = 0 by Th8; :: thesis: verum