:: deftheorem Def1 defines *' POLYRED:def 1 :
for n being Ordinal
for b being bag of n
for L being non empty ZeroStr
for p, b₅ being Series of n,L holds
( b₅ = b *' p iff for b9 being bag of n st b divides b9 holds
( b₅ . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
b₅ . b9 = 0. L ) ) );