let f be S-Sequence_in_R2; :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f . (len f) in L~ (R_Cut (f,p)) holds
f . (len f) = p
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & f . (len f) in L~ (R_Cut (f,p)) implies f . (len f) = p )
assume that
A1: p in L~ f and
A2: f . (len f) in L~ (R_Cut (f,p)) ; :: thesis: f . (len f) = p
A3: L~ f = L~ (Rev f) by SPPOL_2:22;
A4: (Rev f) . 1 = f . (len f) by FINSEQ_5:62;
L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) by A1, JORDAN3:22;
then (Rev f) . 1 in L~ (L_Cut ((Rev f),p)) by A2, A4, SPPOL_2:22;
hence f . (len f) = p by A1, A3, A4, JORDAN1E:7; :: thesis: verum