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 len f <> 0 by TOPREAL1:28;
then A2: not f is empty by CARD_1:47;

now

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

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

then A4: L_Cut f,p = mid f,((Index p,f) + 1),(len f) by Def4;
A5: 1 <= (Index p,f) + 1 by NAT_1:11;
Index p,f < len f by A1, Th41;
then A6: (Index p,f) + 1 <= len f by NAT_1:13;
1 in dom f by A2, FINSEQ_5:6;
then 1 <= len f by FINSEQ_3:27;
hence (L_Cut f,p) . 1 = p by A3, A4, A5, A6, Th27; :: 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 A7: ( 1 < i & 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) ) )
Index p,f < len f by A1, Th41;
then A8: ( 1 <= (Index p,f) + 1 & (Index p,f) + 1 <= len f ) by NAT_1:11, NAT_1:13;
then A9: 1 <= len f by XXREAL_0:2;
A10: len <*p*> <= i by A7, FINSEQ_1:57;
A11: len <*p*> < i by A7, FINSEQ_1:56;
A12: 1 <= i - 1 by A7, SPPOL_1:6;
A13: (i -' 1) + 1 = (i - 1) + 1 by A7, XREAL_1:235
.= i ;

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 A7, A8, A9, Th27
.= f . (((i + (Index p,f)) + 1) -' 1)
.= f . ((Index p,f) + i) by NAT_D:34 ;
:: thesis: verum

end;

assume p <> f . ((Index p,f) + 1) ; :: thesis: (L_Cut f,p) . i = f . (((Index p,f) + i) - 1)
then A14: L_Cut f,p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) by Def4;
then A15: i <= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f))) by A7, FINSEQ_1:35;
len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1 by A8, A9, Th27;
then (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 A8, XREAL_1:235
.= ((len f) - (Index p,f)) + 1 ;
then i - 1 <= (((len f) - (Index p,f)) + 1) - 1 by A15, XREAL_1:11;
then A16: ( 1 <= i -' 1 & i -' 1 <= ((len f) - ((Index p,f) + 1)) + 1 ) by A12, NAT_D:39;
A17: (L_Cut f,p) . i = (mid f,((Index p,f) + 1),(len f)) . (i - (len <*p*>)) by A7, A11, A14, Th15
.= (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 A8, A16, Th31
.= f . (((Index p,f) + i) -' 1) by A13 ;
i <= i + (Index p,f) by NAT_1:11;
hence (L_Cut f,p) . i = f . (((Index p,f) + i) - 1) by A7, A17, XREAL_1:235, XXREAL_0:2; :: thesis: verum