let p be FinSequence; :: thesis: for m, n being Element of NAT st 1 <= m & m <= n & n <= len p holds
( (m,n -cut p) . 1 = p . m & (m,n -cut p) . (len (m,n -cut p)) = p . n )
let m, n be Element of NAT ; :: thesis: ( 1 <= m & m <= n & n <= len p implies ( (m,n -cut p) . 1 = p . m & (m,n -cut p) . (len (m,n -cut p)) = p . n ) )
set c = m,n -cut p;
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len p ; :: thesis: ( (m,n -cut p) . 1 = p . m & (m,n -cut p) . (len (m,n -cut p)) = p . n )
A4: m <= n + 1 by A2, NAT_1:12;
then A5: (len (m,n -cut p)) + m = n + 1 by A1, A3, Lm2;

A6: now

assume len (m,n -cut p) = 0 ; :: thesis: contradiction
then n + 1 <= n + 0 by A2, A5;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

( 0 < len (m,n -cut p) & 0 + 1 = 1 ) by A6;
hence (m,n -cut p) . 1 = p . (m + 0 ) by A1, A3, A4, Lm2
.= p . m ;
:: thesis: (m,n -cut p) . (len (m,n -cut p)) = p . n
0 + 1 <= len (m,n -cut p) by A6, NAT_1:13;
then consider i being Element of NAT such that
A8: ( 0 <= i & i < len (m,n -cut p) & len (m,n -cut p) = i + 1 ) by Th1;
m + i = n by A5, A8;
hence (m,n -cut p) . (len (m,n -cut p)) = p . n by A1, A3, A4, A8, Lm2; :: thesis: verum