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 . (len f) holds

L_Cut (f,p) is being_S-Seq

let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & p <> f . (len f) implies L_Cut (f,p) is being_S-Seq )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: p <> f . (len f) ; :: 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, Th33;

hence L_Cut (f,p) is being_S-Seq ; :: thesis: verum

L_Cut (f,p) is being_S-Seq

let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & p <> f . (len f) implies L_Cut (f,p) is being_S-Seq )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: p <> f . (len f) ; :: 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, Th33;

hence L_Cut (f,p) is being_S-Seq ; :: thesis: verum