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)) /. (len (R_Cut (f,p))) = p
let p be Point of (TOP-REAL 2); :: 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 6
.= p by A1, JORDAN3:24 ;
:: thesis: verum