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:65;
L_Cut (Rev f),p = Rev (R_Cut f,p) by A1, JORDAN3:57;
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:11, SPPOL_2:47; :: thesis: verum