let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds
(L_Cut f,p) /. (len (L_Cut f,p)) = f /. (len f)
let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f implies (L_Cut f,p) /. (len (L_Cut f,p)) = f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: p in L~ f ; :: thesis: (L_Cut f,p) /. (len (L_Cut f,p)) = f /. (len f)
A3: len f in dom f by A1, FINSEQ_5:6;
L_Cut f,p <> {} by A2, JORDAN1E:7;
then len (L_Cut f,p) in dom (L_Cut f,p) by FINSEQ_5:6;
hence (L_Cut f,p) /. (len (L_Cut f,p)) = (L_Cut f,p) . (len (L_Cut f,p)) by PARTFUN1:def 8
.= f . (len f) by A1, A2, JORDAN1B:5
.= f /. (len f) by A3, PARTFUN1:def 8 ;
:: thesis: verum