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:28;
then A4: f <> {} ;
Index p,f < len f by A2, JORDAN3:41;
then A5: (Index p,f) + 1 <= len f by NAT_1:13;
1 in dom f by A4, FINSEQ_5:6;
then f /. 1 in L~ (mid f,((Index p,f) + 1),(len f)) by A3, PARTFUN1:def 8;
then (Index p,f) + 1 = 0 + 1 by A1, A5, JORDAN5B:16, NAT_1:11;
hence contradiction by A2, JORDAN3:41; :: thesis: verum