:: deftheorem BAR defines | BAGORD_2:def 11 :
for I being set
for m being bag of I
for J being set
for b₄ being bag of I holds
( b₄ = m | J iff for i being object st i in I holds
( ( i in J implies b₄ . i = m . i ) & ( not i in J implies b₄ . i = 0 ) ) );