let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds
L_Cut f,p is_S-Seq_joining p,f /. (len f)
let p be Point of (TOP-REAL 2); :: thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 implies L_Cut f,p is_S-Seq_joining p,f /. (len f) )
assume that
A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and
A2: p in L~ f and
A3: p <> f . (len f) and
A4: p <> f . 1 ; :: thesis: L_Cut f,p is_S-Seq_joining p,f /. (len f)
A5: Rev f is special by A1, SPPOL_2:42;
A6: p in L~ (Rev f) by A2, SPPOL_2:22;
p <> (Rev f) . (len f) by A4, FINSEQ_5:65;
then A7: p <> (Rev f) . (len (Rev f)) by FINSEQ_5:def 3;
A8: Rev f is s.n.c. by A1, SPPOL_2:36;
A9: p <> (Rev f) . 1 by A3, FINSEQ_5:65;
A10: Rev f is unfolded by A1, SPPOL_2:29;
L_Cut f,p = L_Cut (Rev (Rev f)),p by FINSEQ_6:29
.= Rev (R_Cut (Rev f),p) by A1, A7, A10, A8, A6, Th38 ;
then L_Cut f,p is_S-Seq_joining p,(Rev f) /. 1 by A1, A5, A10, A8, A6, A9, Th39, JORDAN3:48;
hence L_Cut f,p is_S-Seq_joining p,f /. (len f) by FINSEQ_5:68; :: thesis: verum