theorem Th16: :: BAGORDER:17

for i, j, n being Nat
for a, b being bag of n holds (i,j) -cut (a + b) = ((i,j) -cut a) + ((i,j) -cut b)