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 & p <> f . (len f) ) and
A3: p <> f . 1 ; :: thesis: L_Cut f,p is_S-Seq_joining p,f /. (len f)
p <> (Rev f) . (len f) by A3, FINSEQ_5:65;
then A4: p <> (Rev f) . (len (Rev f)) by FINSEQ_5:def 3;
A5: Rev f is almost-one-to-one FinSequence by A1;
A6: Rev f is special by A1, SPPOL_2:42;
A7: Rev f is unfolded by A1, SPPOL_2:29;
A8: Rev f is s.n.c. by A1, SPPOL_2:36;
A9: p in L~ (Rev f) by A2, SPPOL_2:22;
A10: L_Cut f,p = L_Cut (Rev (Rev f)),p by FINSEQ_6:29
.= Rev (R_Cut (Rev f),p) by A4, A5, A7, A8, A9, Th38 ;
p <> (Rev f) . 1 by A2, FINSEQ_5:65;
then L_Cut f,p is_S-Seq_joining p,(Rev f) /. 1 by A5, A6, A7, A8, A9, A10, Th39, JORDAN3:48;
hence L_Cut f,p is_S-Seq_joining p,f /. (len f) by FINSEQ_5:68; :: thesis: verum