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 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, Th8;
A5: Index (p,f) <= len f by A1, Th8;
i <= len f by A3, NAT_D:46;
then A6: 1 <= len f by A2, XXREAL_0:2;

now :: thesis: ( ( p <> f . 1 & len (R_Cut (f,p)) = (Index (p,f)) + 1 ) or ( p = f . 1 & len (R_Cut (f,p)) = Index (p,f) ) )

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 Def4;
hence len (R_Cut (f,p)) = (len (mid (f,1,(Index (p,f))))) + (len <*p*>) by FINSEQ_1:22
.= (len (mid (f,1,(Index (p,f))))) + 1 by FINSEQ_1:39
.= (((Index (p,f)) -' 1) + 1) + 1 by A6, A4, A5, FINSEQ_6:118
.= (Index (p,f)) + 1 by A1, Th8, XREAL_1:235 ;
:: 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:27, FINSEQ_5:6;
then A9: p = f /. 1 by A7, PARTFUN1:def 6;
R_Cut (f,p) = <*p*> by A7, Def4;
hence len (R_Cut (f,p)) = 1 by FINSEQ_1:39
.= Index (p,f) by A8, A9, Th11 ;
:: 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