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