for p being FinSequence
for m, n, a being Nat st a in dom ((m,n) -cut p) holds
ex k being Nat st
( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )