let f be non empty FinSequence of (TOP-REAL 2); 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); ( 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
; 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; verum