theorem Th21: :: BAGORD_2:32

for I being set holds Sum (<*> (Bags I)) = EmptyBag I