let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds
p in L~ (L_Cut (f,q))
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq implies p in L~ (L_Cut (f,q)) )
assume that
A1: p in L~ f and
A2: q in L~ f and
A3: q <> f . (len f) and
A4: p = f . (len f) and
A5: f is being_S-Seq ; :: thesis: p in L~ (L_Cut (f,q))
1 + 1 <= len f by A5, TOPREAL1:def 8;
then A6: 1 < len f by XXREAL_0:2;
then A7: (Index (p,f)) + 1 = len f by A4, A5, JORDAN3:12;
AA: len f in dom f by A6, FINSEQ_3:25;
then AB: mid (f,(len f),(len f)) = <*(f . (len f))*> by JORDAN4:15
.= <*(f /. (len f))*> by AA, PARTFUN1:def 6 ;
Index (q,f) < len f by A2, JORDAN3:8;
then A8: Index (q,f) <= Index (p,f) by A7, NAT_1:13;