theorem Th67: :: PRE_POLY:69

for n being Ordinal
for b, b1, b2 being bag of n st b = b1 + b2 holds
ex i being Element of NAT st
( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> )