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 A2, XXREAL_0:1;

per cases ( m = n + 1 or m <= n ) by A4, NAT_1:13;

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 n < m by XREAL_1:29;
then (m,n) -cut p = {} by FINSEQ_6:def 4;
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)
( not 1 <= m or not m <= n or not n <= len p ) by A5, XREAL_1:29;
hence for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) by CARD_1:27, FINSEQ_6:def 4; :: 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, FINSEQ_6:def 4; :: thesis: verum

end;

end;