let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st f is being_S-Seq & 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); ( f is being_S-Seq & p in L~ f & p <> f . 1 implies R_Cut (f,p) is_S-Seq_joining f /. 1,p )
assume that
A1:
f is being_S-Seq
and
A2:
p in L~ f
and
A3:
p <> f . 1
; R_Cut (f,p) is_S-Seq_joining f /. 1,p
R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*>
by A3, Def4;
hence
R_Cut (f,p) is_S-Seq_joining f /. 1,p
by A1, A2, A3, Th19; verum