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: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; :: thesis: verum