let f be FinSequence of (TOP-REAL 2); 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); ( 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
; ( ( 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 ( ( 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)
;
len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1then
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
;
verum end; case
p = f . ((Index (p,f)) + 1)
;
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))
;
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 ) )
; verum