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 Element of 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, Th41;
then A5: 1 < (Index p,f) + 1 by NAT_1:13;
Index p,f < len f by A1, Th41;
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:21;

now

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

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 Def4;
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, Th27
.= (((len f) - ((Index p,f) + 1)) + 1) + 1 by A7, XREAL_0:def 2
.= ((len f) - (Index p,f)) + 1 ;
:: thesis: verum

end;

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 Def4;
hence len (L_Cut f,p) = ((len f) -' ((Index p,f) + 1)) + 1 by A4, A5, A6, Th27
.= ((len f) - ((Index p,f) + 1)) + 1 by A7, XREAL_0:def 2
.= (len f) - (Index p,f) ;
:: thesis: verum

end;

end;

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