let p be FinSequence; :: thesis: for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )

let m, n be Nat; :: thesis: ( 1 <= m & m <= n + 1 & n <= len p implies ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) ) )

assume that
A1: 1 <= m and
A2: m <= n + 1 and
A3: n <= len p ; :: thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )

A4: ( m = n + 1 or m < n + 1 ) by ;
per cases ( m = n + 1 or m <= n ) by ;
suppose A5: m = n + 1 ; :: thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )

then A6: n < m by XREAL_1:29;
then (m,n) -cut p = {} by Def1;
hence (len ((m,n) -cut p)) + m = n + 1 by A5; :: thesis: for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i)

thus for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) by ; :: thesis: verum
end;
suppose m <= n ; :: thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )

hence ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) ) by A1, A3, Def1; :: thesis: verum
end;
end;