let p be FinSequence; :: thesis: (1,(len p)) -cut p = p
set cp = (1,(len p)) -cut p;
now :: thesis: ( 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 ; :: 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 ;
then A5: i <= len p by ;
0 + 1 <= i by ;
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 ; :: thesis: verum
end;
hence (1,(len p)) -cut p = p by FINSEQ_2:9; :: thesis: verum