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)
Rev f is being_S-Seq by A1, SPPOL_2:47;
then A3: 2 <= len (Rev f) by TOPREAL1:def 10;
A4: Rev (Rev f) = f by FINSEQ_6:29;
A5: p in L~ (Rev f) by A2, SPPOL_2:22;
then L_Cut (Rev (Rev f)),p = Rev (R_Cut (Rev f),p) by A1, JORDAN3:57, SPPOL_2:47;
hence (L_Cut f,p) . (len (L_Cut f,p)) = (Rev (R_Cut (Rev f),p)) . (len (R_Cut (Rev f),p)) by A4, FINSEQ_5:def 3
.= (R_Cut (Rev f),p) . 1 by FINSEQ_5:65
.= (Rev f) . 1 by A5, A3, Th4, XXREAL_0:2
.= f . (len f) by FINSEQ_5:65 ;
:: thesis: verum