theorem Th4: :: BAGORDER:5

for n, i being Nat
for a, b being ManySortedSet of n holds
( a = b iff ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & ((i + 1),n) -cut a = ((i + 1),n) -cut b ) )