let p be FinSequence; :: thesis: 1,(len p) -cut p = p
set cp = 1,(len p) -cut p;

now

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 ; :: thesis: ( 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 ; :: thesis: for i being Nat st i in dom (1,(len p) -cut p) holds
(1,(len p) -cut p) . i = p . i
let i be Nat; :: thesis: ( 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) ; :: thesis: (1,(len p) -cut p) . i = p . i
A4: dom (1,(len p) -cut p) = Seg (len p) by A2, FINSEQ_1:def 3;
then A5: i <= len p by A3, FINSEQ_1:3;
0 + 1 <= i by A4, A3, FINSEQ_1:3;
then ex k being Element of 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; :: thesis: verum

end;

hence 1,(len p) -cut p = p by FINSEQ_2:10; :: thesis: verum