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 being_S-Seq
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 being_S-Seq )
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 being_S-Seq
L_Cut (f,p) is_S-Seq_joining p,f /. (len f) by A1, A2, A3, A4, Th40;
hence L_Cut (f,p) is being_S-Seq by JORDAN3:def 2; :: thesis: verum