theorem Th15: :: POLYNOM9:15

for X being set
for x being object
for b being bag of X holds b = (b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))