let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( p in L~ f implies (R_Cut (f,p)) /. 1 = f /. 1 )
set i = Index (p,f);
assume A1: p in L~ f ; :: thesis: (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 ;
:: thesis: verum