theorem Lem10: :: BAGORD_2:55

for I being set
for p being Bags b₁ -valued FinSequence st Sum p = EmptyBag I & ( for a being bag of I st a in rng p holds
a <> EmptyBag I ) holds
p = {}