let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 ; :: 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, Def4;

hence R_Cut (f,p) is_S-Seq_joining f /. 1,p by A1, A2, A3, Th19; :: thesis: verum

R_Cut (f,p) is_S-Seq_joining f /. 1,p

let p be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: 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, Def4;

hence R_Cut (f,p) is_S-Seq_joining f /. 1,p by A1, A2, A3, Th19; :: thesis: verum