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:41;
Index p,f <= len f by A1, JORDAN3:41;
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:60;
then 1 <= len (R_Cut f,p) by A1, JORDAN3:41, NAT_1:11;
hence (R_Cut f,p) /. 1 = (R_Cut f,p) . 1 by FINSEQ_4:24
.= f . 1 by A1, A2, JORDAN3:59
.= f /. 1 by A3, PARTFUN1:def 8 ;
:: thesis: verum