let p be FinSequence; :: thesis: for m, n being 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 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 :: thesis: not len ((m,n) -cut p) = 0

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

end;

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