let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for i1 being Nat st f is being_S-Seq & 1 < i1 & i1 <= len f & p = f . i1 holds
(Index p,f) + 1 = i1
let p be Point of (TOP-REAL 2); :: thesis: for i1 being Nat st f is being_S-Seq & 1 < i1 & i1 <= len f & p = f . i1 holds
(Index p,f) + 1 = i1
let i1 be Nat; :: thesis: ( f is being_S-Seq & 1 < i1 & i1 <= len f & p = f . i1 implies (Index p,f) + 1 = i1 )
assume A1:
f is being_S-Seq
; :: thesis: ( not 1 < i1 or not i1 <= len f or not p = f . i1 or (Index p,f) + 1 = i1 )
assume A2:
( 1 < i1 & i1 <= len f )
; :: thesis: ( not p = f . i1 or (Index p,f) + 1 = i1 )
then A3:
i1 in dom f
by FINSEQ_3:27;
consider j being Nat such that
A4:
i1 = j + 1
by A2, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A5:
1 + 0 <= j
by A2, A4, NAT_1:13;
assume
p = f . i1
; :: thesis: (Index p,f) + 1 = i1
then A6:
p = f /. i1
by A3, PARTFUN1:def 8;
then A7:
p in LSeg f,j
by A2, A4, A5, TOPREAL1:27;
then A8:
Index p,f <= j
by Th40;
assume
(Index p,f) + 1 <> i1
; :: thesis: contradiction
then
Index p,f < j
by A4, A8, XXREAL_0:1;
then A9:
(Index p,f) + 1 <= j
by NAT_1:13;
A10:
LSeg f,j c= L~ f
by TOPREAL3:26;
then A11:
p in LSeg f,(Index p,f)
by A7, Th42;
per cases
( (Index p,f) + 1 = j or (Index p,f) + 1 < j )
by A9, XXREAL_0:1;
suppose A12:
(Index p,f) + 1
= j
;
:: thesis: contradictionA13:
f is
unfolded
by A1;
( 1
<= Index p,
f &
(Index p,f) + (1 + 1) <= len f )
by A2, A4, A7, A10, A12, Th41;
then
(LSeg f,(Index p,f)) /\ (LSeg f,j) = {(f /. j)}
by A12, A13, TOPREAL1:def 8;
then
p in {(f /. j)}
by A7, A11, XBOOLE_0:def 4;
then A14:
p = f /. j
by TARSKI:def 1;
A15:
j < i1
by A4, NAT_1:13;
j < len f
by A2, A4, NAT_1:13;
then A16:
j in dom f
by A5, FINSEQ_3:27;
f is
one-to-one
by A1;
hence
contradiction
by A3, A6, A14, A15, A16, PARTFUN2:17;
:: thesis: verum end; suppose A17:
(Index p,f) + 1
< j
;
:: thesis: contradiction
p in (LSeg f,(Index p,f)) /\ (LSeg f,j)
by A7, A11, XBOOLE_0:def 4;
then A18:
LSeg f,
(Index p,f) meets LSeg f,
j
by XBOOLE_0:4;
f is
s.n.c.
by A1;
hence
contradiction
by A17, A18, TOPREAL1:def 9;
:: thesis: verum end;