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 . 1 implies len (R_Cut f,p) = (Index p,f) + 1 ) & ( p = f . 1 implies len (R_Cut f,p) = Index p,f ) )
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ( ( p <> f . 1 implies len (R_Cut f,p) = (Index p,f) + 1 ) & ( p = f . 1 implies len (R_Cut f,p) = Index p,f ) ) )
assume A1: p in L~ f ; :: thesis: ( ( p <> f . 1 implies len (R_Cut f,p) = (Index p,f) + 1 ) & ( p = f . 1 implies len (R_Cut f,p) = Index p,f ) )
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;
A4: 1 <= Index p,f by A1, Th41;
A5: Index p,f <= len f by A1, Th41;
i <= len f by A3, NAT_D:46;
then A6: 1 <= len f by A2, XXREAL_0:2;

now

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

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

then R_Cut f,p = (mid f,1,(Index p,f)) ^ <*p*> by Def5;
hence len (R_Cut f,p) = (len (mid f,1,(Index p,f))) + (len <*p*>) by FINSEQ_1:35
.= (len (mid f,1,(Index p,f))) + 1 by FINSEQ_1:56
.= (((Index p,f) -' 1) + 1) + 1 by A6, A4, A5, Th27
.= (Index p,f) + 1 by A1, Th41, XREAL_1:237 ;
:: thesis: verum

end;

case A7: p = f . 1 ; :: thesis: len (R_Cut f,p) = Index p,f

len f > i by A3, NAT_1:13;
then len f > 1 by A2, XXREAL_0:2;
then A8: len f >= 1 + 1 by NAT_1:13;
1 in dom f by A3, CARD_1:47, FINSEQ_5:6;
then A9: p = f /. 1 by A7, PARTFUN1:def 8;
R_Cut f,p = <*p*> by A7, Def5;
hence len (R_Cut f,p) = 1 by FINSEQ_1:56
.= Index p,f by A8, A9, Th44 ;
:: thesis: verum

end;

end;

end;

hence ( ( p <> f . 1 implies len (R_Cut f,p) = (Index p,f) + 1 ) & ( p = f . 1 implies len (R_Cut f,p) = Index p,f ) ) ; :: thesis: verum