theorem Th27: :: BAGORD_2:38

for I being set
for p being Bags b₁ -valued FinSequence
for i being object st i in support (Sum p) holds
ex b being bag of I st
( b in rng p & i in support b )