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 & p <> f . (len f) holds
L_Cut f,p is_S-Seq_joining p,f /. (len f)
let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & p <> f . (len f) implies L_Cut f,p is_S-Seq_joining p,f /. (len f) )
assume that
A1: ( f is being_S-Seq & p in L~ f ) and
A2: p <> f . (len f) ; :: thesis: L_Cut f,p is_S-Seq_joining p,f /. (len f)
len f <> 0 by A1, TOPREAL1:28;
then A3: f <> {} by CARD_1:47;
A4: ( Rev f is being_S-Seq & p in L~ (Rev f) ) by A1, SPPOL_2:22, SPPOL_2:47;
A5: L_Cut f,p = L_Cut (Rev (Rev f)),p by FINSEQ_6:29
.= Rev (R_Cut (Rev f),p) by A4, Th57 ;
p <> (Rev f) . 1 by A2, FINSEQ_5:65;
then L_Cut f,p is_S-Seq_joining p,(Rev f) /. 1 by A4, A5, Th48, Th67;
hence L_Cut f,p is_S-Seq_joining p,f /. (len f) by A3, FINSEQ_5:68; :: thesis: verum