let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is being_S-Seq implies for p being Point of (TOP-REAL 2) st p in L~ f holds
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) )
assume A1: f is being_S-Seq ; :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f)))
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) )
assume that
A2: p in L~ f and
A3: f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) ; :: thesis: contradiction
len f <> 0 by A2, TOPREAL1:22;
then f <> {} ;
then 1 in dom f by FINSEQ_5:6;
then A4: f /. 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) by A3, PARTFUN1:def 6;
Index (p,f) < len f by A2, JORDAN3:8;
then (Index (p,f)) + 1 <= len f by NAT_1:13;
then (Index (p,f)) + 1 = 0 + 1 by A1, A4, JORDAN5B:16, NAT_1:11;
hence contradiction by A2, JORDAN3:8; :: thesis: verum