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 that
A1: f is being_S-Seq and
A2: p = f . (len f) ; :: thesis: L_Cut (f,p) = <*p*>
len f >= 2 by A1, TOPREAL1:def 8;
then p in L~ f by A2, JORDAN3:1;
then A3: p in L~ (Rev f) by SPPOL_2:22;
A4: L_Cut (f,p) = L_Cut ((Rev (Rev f)),p)
.= Rev (R_Cut ((Rev f),p)) by A1, A3, JORDAN3:22 ;
p = (Rev f) . 1 by A2, FINSEQ_5:62;
then R_Cut ((Rev f),p) = <*p*> by JORDAN3:def 4;
hence L_Cut (f,p) = <*p*> by A4, FINSEQ_5:60; :: thesis: verum