:: deftheorem Def7 defines Constant POLYNOM7:def 7 :
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is Constant iff for b being bag of X st b <> EmptyBag X holds
p . b = 0. L );