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:40;
A6: p in L~ (Rev f) by A2, SPPOL_2:22;
p <> (Rev f) . (len f) by A4, FINSEQ_5:62;
then A7: p <> (Rev f) . (len (Rev f)) by FINSEQ_5:def 3;
A8: Rev f is s.n.c. by A1, SPPOL_2:35;
A9: p <> (Rev f) . 1 by A3, FINSEQ_5:62;
A10: Rev f is unfolded by A1, SPPOL_2:28;
L_Cut (f,p) = L_Cut ((Rev (Rev f)),p)
.= 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:15;
hence L_Cut (f,p) is_S-Seq_joining p,f /. (len f) by FINSEQ_5:65; :: thesis: verum