theorem Th22: :: BAGORD_2:33

for I being set
for p being Bags b₁ -valued FinSequence
for b being bag of I holds Sum (p ^ <*b*>) = (Sum p) + b