let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p in L~ f holds
(R_Cut (f,p)) /. 1 = f /. 1
let p be Point of (TOP-REAL 2); ( p in L~ f implies (R_Cut (f,p)) /. 1 = f /. 1 )
set i = Index (p,f);
assume A1:
p in L~ f
; (R_Cut (f,p)) /. 1 = f /. 1
then A2:
1 <= Index (p,f)
by JORDAN3:8;
Index (p,f) <= len f
by A1, JORDAN3:8;
then
f <> {}
by A2;
then A3:
1 in dom f
by FINSEQ_5:6;
( p = f . 1 or p <> f . 1 )
;
then
( len (R_Cut (f,p)) = Index (p,f) or len (R_Cut (f,p)) = (Index (p,f)) + 1 )
by A1, JORDAN3:25;
then
1 <= len (R_Cut (f,p))
by A1, JORDAN3:8, NAT_1:11;
hence (R_Cut (f,p)) /. 1 =
(R_Cut (f,p)) . 1
by FINSEQ_4:15
.=
f . 1
by A1, A2, JORDAN3:24
.=
f /. 1
by A3, PARTFUN1:def 6
;
verum