let f be FinSequence of (); :: thesis: for p being Point of () 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 (); :: 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 ;
A5: Index (p,f) <= len f by ;
i <= len f by ;
then A6: 1 <= len f by ;
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))))) + () by FINSEQ_1:22
.= (len (mid (f,1,(Index (p,f))))) + 1 by FINSEQ_1:39
.= (((Index (p,f)) -' 1) + 1) + 1 by
.= (Index (p,f)) + 1 by ;
:: thesis: verum
end;
case A7: p = f . 1 ; :: thesis: len (R_Cut (f,p)) = Index (p,f)
len f > i by ;
then len f > 1 by ;
then A8: len f >= 1 + 1 by NAT_1:13;
1 in dom f by ;
then A9: p = f /. 1 by ;
R_Cut (f,p) = <*p*> by ;
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