:: deftheorem Def16 defines decomp PRE_POLY:def 17 :
for n being Ordinal
for b being bag of n
for b₃ being FinSequence of 2 -tuples_on (Bags n) holds
( b₃ = decomp b iff ( dom b₃ = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b₃ & p = (divisors b) /. i holds
b₃ /. i = <*p,(b -' p)*> ) ) );