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 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 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 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 Th8;

then A2: (Index (p,f)) + 1 <= len f by NAT_1:13;

A3: not f is empty by A1, CARD_1:27, TOPREAL1:22;

( ( 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 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:40;

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:118;

then A13: (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) = 1 + (((len f) -' ((Index (p,f)) + 1)) + 1) by FINSEQ_1:40

.= 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by A2, XREAL_1:233

.= ((len f) - (Index (p,f))) + 1 ;

A14: (i -' 1) + 1 = (i - 1) + 1 by A8, XREAL_1:233

.= i ;

A15: 1 <= i - 1 by A8, SPPOL_1:1;

then A16: 1 <= i -' 1 by NAT_D:39;

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 Def3;

then i <= (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A9, FINSEQ_1:22;

then i - 1 <= (((len f) - (Index (p,f))) + 1) - 1 by A13, XREAL_1:9;

then A19: i -' 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A15, NAT_D:39;

len <*p*> < i by A8, FINSEQ_1:39;

then (L_Cut (f,p)) . i = (mid (f,((Index (p,f)) + 1),(len f))) . (i - (len <*p*>)) by A9, A18, FINSEQ_6:108

.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' (len <*p*>)) by A10, XREAL_1:233

.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' 1) by FINSEQ_1:39

.= f . (((i -' 1) + ((Index (p,f)) + 1)) -' 1) by A11, A2, A16, A19, FINSEQ_6:122

.= 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:233, XXREAL_0:2; :: thesis: verum

( (L_Cut (f,p)) . 1 = p & ( for i being 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 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 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 Th8;

then A2: (Index (p,f)) + 1 <= len f by NAT_1:13;

A3: not f is empty by A1, CARD_1:27, TOPREAL1:22;

now :: thesis: (L_Cut (f,p)) . 1 = pend;

hence
(L_Cut (f,p)) . 1 = p
; :: thesis: for i being Nat st 1 < i & i <= len (L_Cut (f,p)) holds per cases
( p = f . ((Index (p,f)) + 1) or p <> f . ((Index (p,f)) + 1) )
;

end;

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:25;

Index (p,f) < len f by A1, Th8;

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, Def3;

hence (L_Cut (f,p)) . 1 = p by A4, A7, A6, A5, FINSEQ_6:118; :: thesis: verum

end;then A5: 1 <= len f by FINSEQ_3:25;

Index (p,f) < len f by A1, Th8;

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, Def3;

hence (L_Cut (f,p)) . 1 = p by A4, A7, A6, A5, FINSEQ_6:118; :: thesis: verum

( ( 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 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:40;

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:118;

then A13: (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) = 1 + (((len f) -' ((Index (p,f)) + 1)) + 1) by FINSEQ_1:40

.= 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by A2, XREAL_1:233

.= ((len f) - (Index (p,f))) + 1 ;

A14: (i -' 1) + 1 = (i - 1) + 1 by A8, XREAL_1:233

.= i ;

A15: 1 <= i - 1 by A8, SPPOL_1:1;

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) )

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)

then L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by Def3;

hence (L_Cut (f,p)) . i = f . ((i + ((Index (p,f)) + 1)) -' 1) by A8, A9, A11, A2, A12, FINSEQ_6:118

.= f . (((i + (Index (p,f))) + 1) -' 1)

.= f . ((Index (p,f)) + i) by NAT_D:34 ;

:: thesis: verum

end;then L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by Def3;

hence (L_Cut (f,p)) . i = f . ((i + ((Index (p,f)) + 1)) -' 1) by A8, A9, A11, A2, A12, FINSEQ_6:118

.= f . (((i + (Index (p,f))) + 1) -' 1)

.= f . ((Index (p,f)) + i) by NAT_D:34 ;

:: thesis: verum

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 Def3;

then i <= (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A9, FINSEQ_1:22;

then i - 1 <= (((len f) - (Index (p,f))) + 1) - 1 by A13, XREAL_1:9;

then A19: i -' 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A15, NAT_D:39;

len <*p*> < i by A8, FINSEQ_1:39;

then (L_Cut (f,p)) . i = (mid (f,((Index (p,f)) + 1),(len f))) . (i - (len <*p*>)) by A9, A18, FINSEQ_6:108

.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' (len <*p*>)) by A10, XREAL_1:233

.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' 1) by FINSEQ_1:39

.= f . (((i -' 1) + ((Index (p,f)) + 1)) -' 1) by A11, A2, A16, A19, FINSEQ_6:122

.= 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:233, XXREAL_0:2; :: thesis: verum