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

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