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 10;
then len f >= 1 by XXREAL_0:2;
then len f in dom f by FINSEQ_3:27;
then p = f . (len f) by A2, PARTFUN1:def 8;
then L_Cut f,p = <*p*> by A1, JORDAN5B:17;
then len (L_Cut f,p) = 1 by FINSEQ_1:56;
hence L~ (L_Cut f,p) = {} by TOPREAL1:28; :: thesis: verum