let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: 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; :: thesis: ( 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. ) ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: (Index (p,f)) + 1 = i1
assume A7: (Index (p,f)) + 1 <> i1 ; :: thesis: 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 ; :: thesis: contradiction

A14: 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; :: thesis: verum

end;

suppose A18: (Index (p,f)) + 1 < j ; :: thesis: 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; :: thesis: verum

end;

end;