let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f . (len f) holds
L_Cut f,p = <*p*>
let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p = f . (len f) implies L_Cut f,p = <*p*> )
assume A1: ( f is being_S-Seq & p = f . (len f) ) ; :: thesis: L_Cut f,p = <*p*>
then len f >= 2 by TOPREAL1:def 10;
then p in L~ f by A1, JORDAN3:34;
then A2: p in L~ (Rev f) by SPPOL_2:22;
A3: L_Cut f,p = L_Cut (Rev (Rev f)),p by FINSEQ_6:29
.= Rev (R_Cut (Rev f),p) by A1, A2, JORDAN3:57, SPPOL_2:47 ;
p = (Rev f) . 1 by A1, FINSEQ_5:65;
then R_Cut (Rev f),p = <*p*> by JORDAN3:def 5;
hence L_Cut f,p = <*p*> by A3, FINSEQ_5:63; :: thesis: verum