let p be FinSequence; :: thesis: for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) )
let m, n be Element of NAT ; :: thesis: ( 1 <= m & m <= n + 1 & n <= len p implies ( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) ) )
assume A1: ( 1 <= m & m <= n + 1 & n <= len p ) ; :: thesis: ( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) )
A2: ( m = n + 1 or m < n + 1 ) by A1, XXREAL_0:1;

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

suppose A3: m = n + 1 ; :: thesis: ( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) )

then A4: n < m by XREAL_1:31;
then m,n -cut p = {} by Def1;
hence (len (m,n -cut p)) + m = n + 1 by A3, CARD_1:47; :: thesis: for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i)
thus for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) by A4, Def1, CARD_1:47; :: thesis: verum

end;

suppose m <= n ; :: thesis: ( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of 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 Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) ) by A1, Def1; :: thesis: verum

end;

end;