theorem Th24: :: BAGORD_2:35
for I being set
for p, q being Bags b1 -valued FinSequence holds Sum (p ^ q) = (Sum p) + (Sum q)