theorem Th21: :: BAGORD_2:32
for I being set holds Sum (<*> (Bags I)) = EmptyBag I