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

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