let p be FinSequence; 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; ( 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
; ( ((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;
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
;
((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; verum