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;
A5: ( not 1 <= m or not m <= n or not n <= len p ) by A3, XREAL_1:31;
m,n -cut p = {} by A4, GRAPH_2:def 1;
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 A5, CARD_1:47, GRAPH_2:def 1; :: 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, GRAPH_2:def 1; :: thesis: verum

end;

end;