let f be 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 . 1 holds
R_Cut f,p is_S-Seq_joining f /. 1,p
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 . 1 implies R_Cut f,p is_S-Seq_joining f /. 1,p )
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 . 1 ; :: thesis: R_Cut f,p is_S-Seq_joining f /. 1,p
R_Cut f,p = (mid f,1,(Index p,f)) ^ <*p*> by A3, JORDAN3:def 5;
hence R_Cut f,p is_S-Seq_joining f /. 1,p by A1, A2, A3, Th35; :: thesis: verum