let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2)
for i1 being Nat st f is poorly-one-to-one & f is unfolded & f is s.n.c. & 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 poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 holds
(Index (p,f)) + 1 = i1
let i1 be Nat; ( f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 implies (Index (p,f)) + 1 = i1 )
assume A1:
( f is poorly-one-to-one & f is unfolded & f is s.n.c. )
; ( 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 )
consider j being Nat such that
A4:
i1 = j + 1
by A2, NAT_1:6;
reconsider j = j as Nat ;
A5:
1 + 0 <= j
by A2, A4, NAT_1:13;
assume A6:
p = f . i1
; (Index (p,f)) + 1 = i1
assume A7:
(Index (p,f)) + 1 <> i1
; contradiction
A8:
j in NAT
by ORDINAL1:def 12;
i1 in dom f
by A2, A3, FINSEQ_3:25;
then
p = f /. i1
by A6, PARTFUN1:def 6;
then A9:
p in LSeg (f,j)
by A3, A4, A5, TOPREAL1:21;
then
Index (p,f) <= j
by A8, JORDAN3:7;
then
Index (p,f) < j
by A4, A7, 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, JORDAN3:9;
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
;
contradictionA14:
1
<= Index (
p,
f)
by A9, A11, JORDAN3:8;
then
(Index (p,f)) + 2
>= 1
+ 2
by XREAL_1:7;
then
len f >= 2
+ 1
by A3, A4, A13, XXREAL_0:2;
then A15:
len f > 2
by NAT_1:13;
(Index (p,f)) + (1 + 1) <= len f
by A3, A4, A13;
then
(LSeg (f,(Index (p,f)))) /\ (LSeg (f,j)) = {(f /. j)}
by A1, A13, A14, TOPREAL1:def 6;
then A16:
p in {(f /. j)}
by A9, A12, XBOOLE_0:def 4;
A17:
j < len f
by A3, A4, NAT_1:13;
then
j in dom f
by A5, FINSEQ_3:25;
then f . j =
f /. j
by PARTFUN1:def 6
.=
f . i1
by A6, A16, TARSKI:def 1
;
hence
contradiction
by A1, A4, A5, A17, A15, Def3;
verum end; suppose A18:
(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)
;
hence
contradiction
by A1, A18, TOPREAL1:def 7;
verum end; end;