let f be FinSequence of (TOP-REAL 2); 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); 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; ( 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
; ( not 1 < i1 or not i1 <= len f or not p = f . i1 or (Index (p,f)) + 1 = i1 )
assume that
A2:
1 < i1
and
A3:
i1 <= len f
; ( not p = f . i1 or (Index (p,f)) + 1 = i1 )
A4:
i1 in dom f
by A2, A3, FINSEQ_3:25;
assume
p = f . i1
; (Index (p,f)) + 1 = i1
then A5:
p = f /. i1
by A4, PARTFUN1:def 6;
assume A6:
(Index (p,f)) + 1 <> i1
; contradiction
consider j being Nat such that
A7:
i1 = j + 1
by A2, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
A8:
1 + 0 <= j
by A2, A7, NAT_1:13;
then A9:
p in LSeg (f,j)
by A3, A7, A5, TOPREAL1:21;
then
Index (p,f) <= j
by Th7;
then
Index (p,f) < j
by A7, A6, XXREAL_0:1;
then A10:
(Index (p,f)) + 1 <= j
by NAT_1:13;
A11:
LSeg (f,j) c= L~ f
by TOPREAL3:19;
then A12:
p in LSeg (f,(Index (p,f)))
by A9, Th9;
per cases
( (Index (p,f)) + 1 = j or (Index (p,f)) + 1 < j )
by A10, XXREAL_0:1;
suppose A13:
(Index (p,f)) + 1
= j
;
contradictionthen A14:
(Index (p,f)) + (1 + 1) <= len f
by A3, A7;
1
<= Index (
p,
f)
by A9, A11, Th8;
then
(LSeg (f,(Index (p,f)))) /\ (LSeg (f,j)) = {(f /. j)}
by A1, A13, A14, TOPREAL1:def 6;
then
p in {(f /. j)}
by A9, A12, XBOOLE_0:def 4;
then A15:
p = f /. j
by TARSKI:def 1;
j < len f
by A3, A7, NAT_1:13;
then A16:
j in dom f
by A8, FINSEQ_3:25;
j < i1
by A7, NAT_1:13;
hence
contradiction
by A1, A4, A5, A15, A16, PARTFUN2:10;
verum end; suppose A17:
(Index (p,f)) + 1
< j
;
contradiction
p in (LSeg (f,(Index (p,f)))) /\ (LSeg (f,j))
by A9, A12, XBOOLE_0:def 4;
then
LSeg (
f,
(Index (p,f)))
meets LSeg (
f,
j)
by XBOOLE_0:4;
hence
contradiction
by A1, A17, TOPREAL1:def 7;
verum end;