:: deftheorem Def10 defines * POLYNOM7:def 10 :
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₅ = p * a iff for b being bag of X holds b₅ . b = (p . b) * a );