let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
( (L_Cut f,p) . 1 = p & ( for i being Element of NAT st 1 < i & i <= len (L_Cut f,p) holds
( ( p = f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . ((Index p,f) + i) ) & ( p <> f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) ) ) ) )
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ( (L_Cut f,p) . 1 = p & ( for i being Element of NAT st 1 < i & i <= len (L_Cut f,p) holds
( ( p = f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . ((Index p,f) + i) ) & ( p <> f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) ) ) ) ) )
assume A1: p in L~ f ; :: thesis: ( (L_Cut f,p) . 1 = p & ( for i being Element of NAT st 1 < i & i <= len (L_Cut f,p) holds
( ( p = f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . ((Index p,f) + i) ) & ( p <> f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) ) ) ) )
then Index p,f < len f by Th41;
then A2: (Index p,f) + 1 <= len f by NAT_1:13;
A3: not f is empty by A1, CARD_1:47, TOPREAL1:28;

now

per cases ( p = f . ((Index p,f) + 1) or p <> f . ((Index p,f) + 1) ) ;

suppose A4: p = f . ((Index p,f) + 1) ; :: thesis: (L_Cut f,p) . 1 = p

1 in dom f by A3, FINSEQ_5:6;
then A5: 1 <= len f by FINSEQ_3:27;
Index p,f < len f by A1, Th41;
then A6: (Index p,f) + 1 <= len f by NAT_1:13;
A7: 1 <= (Index p,f) + 1 by NAT_1:11;
L_Cut f,p = mid f,((Index p,f) + 1),(len f) by A4, Def4;
hence (L_Cut f,p) . 1 = p by A4, A7, A6, A5, FINSEQ_6:124; :: thesis: verum

end;

suppose p <> f . ((Index p,f) + 1) ; :: thesis: (L_Cut f,p) . 1 = p

then L_Cut f,p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) by Def4;
hence (L_Cut f,p) . 1 = p by FINSEQ_1:58; :: thesis: verum

end;

end;

end;

hence (L_Cut f,p) . 1 = p ; :: thesis: for i being Element of NAT st 1 < i & i <= len (L_Cut f,p) holds
( ( p = f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . ((Index p,f) + i) ) & ( p <> f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) ) )
let i be Element of NAT ; :: thesis: ( 1 < i & i <= len (L_Cut f,p) implies ( ( p = f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . ((Index p,f) + i) ) & ( p <> f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) ) ) )
assume that
A8: 1 < i and
A9: i <= len (L_Cut f,p) ; :: thesis: ( ( p = f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . ((Index p,f) + i) ) & ( p <> f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) ) )
A10: len <*p*> <= i by A8, FINSEQ_1:57;
A11: 1 <= (Index p,f) + 1 by NAT_1:11;
then A12: 1 <= len f by A2, XXREAL_0:2;
then len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1 by A11, A2, FINSEQ_6:124;
then A13: (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f))) = 1 + (((len f) -' ((Index p,f) + 1)) + 1) by FINSEQ_1:57
.= 1 + (((len f) - ((Index p,f) + 1)) + 1) by A2, XREAL_1:235
.= ((len f) - (Index p,f)) + 1 ;
A14: (i -' 1) + 1 = (i - 1) + 1 by A8, XREAL_1:235
.= i ;
A15: 1 <= i - 1 by A8, SPPOL_1:6;
then A16: 1 <= i -' 1 by NAT_D:39;

hereby :: thesis: ( p <> f . ((Index p,f) + 1) implies (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) )

assume p = f . ((Index p,f) + 1) ; :: thesis: (L_Cut f,p) . i = f . ((Index p,f) + i)
then L_Cut f,p = mid f,((Index p,f) + 1),(len f) by Def4;
hence (L_Cut f,p) . i = f . ((i + ((Index p,f) + 1)) -' 1) by A8, A9, A11, A2, A12, FINSEQ_6:124
.= f . (((i + (Index p,f)) + 1) -' 1)
.= f . ((Index p,f) + i) by NAT_D:34 ;
:: thesis: verum

end;

A17: i <= i + (Index p,f) by NAT_1:11;
assume p <> f . ((Index p,f) + 1) ; :: thesis: (L_Cut f,p) . i = f . (((Index p,f) + i) - 1)
then A18: L_Cut f,p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) by Def4;
then i <= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f))) by A9, FINSEQ_1:35;
then i - 1 <= (((len f) - (Index p,f)) + 1) - 1 by A13, XREAL_1:11;
then A19: i -' 1 <= ((len f) - ((Index p,f) + 1)) + 1 by A15, NAT_D:39;
len <*p*> < i by A8, FINSEQ_1:56;
then (L_Cut f,p) . i = (mid f,((Index p,f) + 1),(len f)) . (i - (len <*p*>)) by A9, A18, FINSEQ_6:114
.= (mid f,((Index p,f) + 1),(len f)) . (i -' (len <*p*>)) by A10, XREAL_1:235
.= (mid f,((Index p,f) + 1),(len f)) . (i -' 1) by FINSEQ_1:56
.= f . (((i -' 1) + ((Index p,f) + 1)) -' 1) by A11, A2, A16, A19, FINSEQ_6:128
.= f . (((Index p,f) + i) -' 1) by A14 ;
hence (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) by A8, A17, XREAL_1:235, XXREAL_0:2; :: thesis: verum