:: deftheorem PART defines partition BAGORD_2:def 8 :
for I being set
for b being bag of I
for b₃ being Bags b₁ -valued FinSequence holds
( b₃ is partition of b iff b = Sum b₃ );