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 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, Th8;
then A5: 1 < (Index (p,f)) + 1 by NAT_1:13;
Index (p,f) < len f by A1, Th8;
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:19;
now :: thesis: ( ( p <> f . ((Index (p,f)) + 1) & len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) or ( p = f . ((Index (p,f)) + 1) & len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) )
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 Def3;
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, FINSEQ_6:118
.= (((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 Def3;
hence len (L_Cut (f,p)) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A4, A5, A6, FINSEQ_6:118
.= ((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