:: deftheorem Def1 defines -cut FINSEQ_6:def 4 :
for p being FinSequence
for m, n being Nat
for b₄ being FinSequence holds
( ( 1 <= m & m <= n & n <= len p implies ( b₄ = (m,n) -cut p iff ( (len b₄) + m = n + 1 & ( for i being Nat st i < len b₄ holds
b₄ . (i + 1) = p . (m + i) ) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ( b₄ = (m,n) -cut p iff b₄ = {} ) ) );