theorem Th28: :: BAGORD_2:40

for I being set
for p being Bags b₁ -valued FinSequence
for a, b being bag of I holds
( <*a*> ^ p is partition of b iff ( a divides b & p is partition of b -' a ) )