let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2)
for i1 being Element of 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 Element of 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 Element of 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 Element of NAT by ORDINAL1:def 13;
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
i1 in dom f
by A2, A3, FINSEQ_3:27;
then
p = f /. i1
by A6, PARTFUN1:def 8;
then A8:
p in LSeg f,j
by A3, A4, A5, TOPREAL1:27;
then
Index p,f <= j
by JORDAN3:40;
then
Index p,f < j
by A4, A7, 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 A8, JORDAN3:42;
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
;
contradictionA13:
1
<= Index p,
f
by A8, A10, JORDAN3:41;
then
(Index p,f) + 2
>= 1
+ 2
by XREAL_1:9;
then
len f >= 2
+ 1
by A3, A4, A12, XXREAL_0:2;
then A14:
len f > 2
by NAT_1:13;
(Index p,f) + (1 + 1) <= len f
by A3, A4, A12;
then
(LSeg f,(Index p,f)) /\ (LSeg f,j) = {(f /. j)}
by A1, A12, A13, TOPREAL1:def 8;
then A15:
p in {(f /. j)}
by A8, A11, XBOOLE_0:def 4;
A16:
j < len f
by A3, A4, NAT_1:13;
then
j in dom f
by A5, FINSEQ_3:27;
then f . j =
f /. j
by PARTFUN1:def 8
.=
f . i1
by A6, A15, TARSKI:def 1
;
hence
contradiction
by A1, A4, A5, A16, A14, Def3;
verum end; suppose A17:
(Index p,f) + 1
< j
;
contradiction
p in (LSeg f,(Index p,f)) /\ (LSeg f,j)
by A8, A11, 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 9;
verum end;