for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( degree p = 0 iff Support p c= {(EmptyBag n)} )