let f be FinSequence of ; :: thesis: for p being Point of st p in L~ f holds
(R_Cut f,p) /. (len (R_Cut f,p)) = p
let p be Point of ; :: thesis: ( p in L~ f implies (R_Cut f,p) /. (len (R_Cut f,p)) = p )
assume A1: p in L~ f ; :: thesis: (R_Cut f,p) /. (len (R_Cut f,p)) = p
not R_Cut f,p is empty by Th44;
then len (R_Cut f,p) in dom (R_Cut f,p) by FINSEQ_5:6;
hence (R_Cut f,p) /. (len (R_Cut f,p)) = (R_Cut f,p) . (len (R_Cut f,p)) by PARTFUN1:def 8
.= p by A1, JORDAN3:59 ;
:: thesis: verum