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 and
A2: p in L~ f and
A3: p <> f . (len f) ; :: thesis: L_Cut (f,p) is_S-Seq_joining p,f /. (len f)
A4: f <> {} by A2, CARD_1:27, TOPREAL1:22;
A5: Rev f is being_S-Seq by A1;
A6: p in L~ (Rev f) by A2, SPPOL_2:22;
A7: p <> (Rev f) . 1 by A3, FINSEQ_5:62;
L_Cut (f,p) = L_Cut ((Rev (Rev f)),p)
.= Rev (R_Cut ((Rev f),p)) by A1, A6, Th22 ;
then L_Cut (f,p) is_S-Seq_joining p,(Rev f) /. 1 by A5, A6, A7, Th15, Th32;
hence L_Cut (f,p) is_S-Seq_joining p,f /. (len f) by A4, FINSEQ_5:65; :: thesis: verum