theorem Th25: :: BAGORD_2:36

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