:: deftheorem Def9 defines * POLYNOM7:def 9 :
for X being set
for L being non empty multLoopStr_0
for p being Series of X,L
for a being Element of L
for b₅ being Series of X,L holds
( b₅ = a * p iff for b being bag of X holds b₅ . b = a * (p . b) );