:: deftheorem Def10 defines *' POLYNOM1:def 10 :
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p, q, b₅ being Series of n,L holds
( b₅ = p *' q iff for b being bag of n ex s being FinSequence of the carrier of L st
( b₅ . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) );