:: deftheorem defines | POLYNOM7:def 8 :
for X being set
for L being non empty ZeroStr
for a being Element of L holds a | (X,L) = (0_ (X,L)) +* ((EmptyBag X),a);