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;

( ( 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) ) )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: verumper cases
( p <> f . 1 or p = f . 1 )
;

end;

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;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

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;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