:: deftheorem defines Monom POLYNOM7:def 4 :
for X being set
for L being non empty ZeroStr
for a being Element of L
for b being bag of X holds Monom (a,b) = (0_ (X,L)) +* (b,a);