let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f /. (len f) holds

L~ (L_Cut (f,p)) = {}

let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p = f /. (len f) implies L~ (L_Cut (f,p)) = {} )

assume that

A1: f is being_S-Seq and

A2: p = f /. (len f) ; :: thesis: L~ (L_Cut (f,p)) = {}

len f >= 2 by A1, TOPREAL1:def 8;

then len f >= 1 by XXREAL_0:2;

then len f in dom f by FINSEQ_3:25;

then p = f . (len f) by A2, PARTFUN1:def 6;

then L_Cut (f,p) = <*p*> by A1, JORDAN5B:17;

then len (L_Cut (f,p)) = 1 by FINSEQ_1:39;

hence L~ (L_Cut (f,p)) = {} by TOPREAL1:22; :: thesis: verum

L~ (L_Cut (f,p)) = {}

let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p = f /. (len f) implies L~ (L_Cut (f,p)) = {} )

assume that

A1: f is being_S-Seq and

A2: p = f /. (len f) ; :: thesis: L~ (L_Cut (f,p)) = {}

len f >= 2 by A1, TOPREAL1:def 8;

then len f >= 1 by XXREAL_0:2;

then len f in dom f by FINSEQ_3:25;

then p = f . (len f) by A2, PARTFUN1:def 6;

then L_Cut (f,p) = <*p*> by A1, JORDAN5B:17;

then len (L_Cut (f,p)) = 1 by FINSEQ_1:39;

hence L~ (L_Cut (f,p)) = {} by TOPREAL1:22; :: thesis: verum