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:3;
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 6
.= f . (len f) by A1, A2, JORDAN1B:4
.= f /. (len f) by A3, PARTFUN1:def 6 ;
:: thesis: verum