let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds

( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) )

let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) ) )

assume A1: p in L~ f ; :: thesis: ( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) )

then consider i being Nat such that

A2: 1 <= i and

A3: i + 1 <= len f and

p in LSeg (f,i) by SPPOL_2:13;

i <= len f by A3, NAT_D:46;

then A4: 1 <= len f by A2, XXREAL_0:2;

1 <= Index (p,f) by A1, Th8;

then A5: 1 < (Index (p,f)) + 1 by NAT_1:13;

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

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

then A7: (len f) - ((Index (p,f)) + 1) >= 0 by XREAL_1:19;

( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) )

let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) ) )

assume A1: p in L~ f ; :: thesis: ( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) )

then consider i being Nat such that

A2: 1 <= i and

A3: i + 1 <= len f and

p in LSeg (f,i) by SPPOL_2:13;

i <= len f by A3, NAT_D:46;

then A4: 1 <= len f by A2, XXREAL_0:2;

1 <= Index (p,f) by A1, Th8;

then A5: 1 < (Index (p,f)) + 1 by NAT_1:13;

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

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

then A7: (len f) - ((Index (p,f)) + 1) >= 0 by XREAL_1:19;

now :: thesis: ( ( p <> f . ((Index (p,f)) + 1) & len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) or ( p = f . ((Index (p,f)) + 1) & len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) )end;

hence
( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) )
; :: thesis: verumper cases
( p <> f . ((Index (p,f)) + 1) or p = f . ((Index (p,f)) + 1) )
;

end;

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

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

hence len (L_Cut (f,p)) = 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_5:8

.= (((len f) -' ((Index (p,f)) + 1)) + 1) + 1 by A4, A5, A6, FINSEQ_6:118

.= (((len f) - ((Index (p,f)) + 1)) + 1) + 1 by A7, XREAL_0:def 2

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

:: thesis: verum

end;hence len (L_Cut (f,p)) = 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_5:8

.= (((len f) -' ((Index (p,f)) + 1)) + 1) + 1 by A4, A5, A6, FINSEQ_6:118

.= (((len f) - ((Index (p,f)) + 1)) + 1) + 1 by A7, XREAL_0:def 2

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

:: thesis: verum

case
p = f . ((Index (p,f)) + 1)
; :: thesis: len (L_Cut (f,p)) = (len f) - (Index (p,f))

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

hence len (L_Cut (f,p)) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A4, A5, A6, FINSEQ_6:118

.= ((len f) - ((Index (p,f)) + 1)) + 1 by A7, XREAL_0:def 2

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

:: thesis: verum

end;hence len (L_Cut (f,p)) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A4, A5, A6, FINSEQ_6:118

.= ((len f) - ((Index (p,f)) + 1)) + 1 by A7, XREAL_0:def 2

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

:: thesis: verum