:: deftheorem Def1 defines -cut BAGORDER:def 1 :
for n, i, j being Nat
for b being ManySortedSet of n
for b₅ being ManySortedSet of j -' i holds
( b₅ = (i,j) -cut b iff for k being Element of NAT st k in j -' i holds
b₅ . k = b . (i + k) );