let p be FinSequence; (1,(len p)) -cut p = p
set cp = (1,(len p)) -cut p;
now ( len ((1,(len p)) -cut p) = len p & len p = len p & ( for i being Nat st i in dom ((1,(len p)) -cut p) holds
((1,(len p)) -cut p) . i = p . i ) )A1:
1
<= (len p) + 1
by NAT_1:11;
then A2:
(len ((1,(len p)) -cut p)) + 1
= (len p) + 1
by Lm2;
hence
len ((1,(len p)) -cut p) = len p
;
( len p = len p & ( for i being Nat st i in dom ((1,(len p)) -cut p) holds
((1,(len p)) -cut p) . i = p . i ) )thus
len p = len p
;
for i being Nat st i in dom ((1,(len p)) -cut p) holds
((1,(len p)) -cut p) . i = p . ilet i be
Nat;
( i in dom ((1,(len p)) -cut p) implies ((1,(len p)) -cut p) . i = p . i )assume A3:
i in dom ((1,(len p)) -cut p)
;
((1,(len p)) -cut p) . i = p . iA4:
dom ((1,(len p)) -cut p) = Seg (len p)
by A2, FINSEQ_1:def 3;
then A5:
i <= len p
by A3, FINSEQ_1:1;
0 + 1
<= i
by A4, A3, FINSEQ_1:1;
then
ex
k being
Nat st
(
0 <= k &
k < len ((1,(len p)) -cut p) &
i = k + 1 )
by A2, A5, Th1;
hence
((1,(len p)) -cut p) . i = p . i
by A1, Lm2;
verum end;
hence
(1,(len p)) -cut p = p
by FINSEQ_2:9; verum