theorem Th23: :: BAGORD_2:34

for I being set
for b being bag of I holds Sum <*b*> = b