let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for i1 being Element of NAT st f is unfolded & f is s.n.c. & i1 + 1 <= len f & p in LSeg f,i1 & p <> f . i1 holds
i1 = Index p,f
let p be Point of (TOP-REAL 2); :: thesis: for i1 being Element of NAT st f is unfolded & f is s.n.c. & i1 + 1 <= len f & p in LSeg f,i1 & p <> f . i1 holds
i1 = Index p,f
let i1 be Element of NAT ; :: thesis: ( f is unfolded & f is s.n.c. & i1 + 1 <= len f & p in LSeg f,i1 & p <> f . i1 implies i1 = Index p,f )
assume that
A1: ( f is unfolded & f is s.n.c. ) and
A2: i1 + 1 <= len f and
A3: p in LSeg f,i1 ; :: thesis: ( not p <> f . i1 or i1 = Index p,f )
A4: i1 < len f by A2, NAT_1:13;
A5: 1 <= (Index p,f) + 1 by NAT_1:11;
Index p,f <= i1 by A3, Th40;
then Index p,f < len f by A4, XXREAL_0:2;
then (Index p,f) + 1 <= len f by NAT_1:13;
then A6: (Index p,f) + 1 in dom f by A5, FINSEQ_3:27;
assume A7: p <> f . i1 ; :: thesis: i1 = Index p,f
A8: p in L~ f by A3, SPPOL_2:17;
then p in LSeg f,(Index p,f) by Th42;
then A9: p in (LSeg f,(Index p,f)) /\ (LSeg f,i1) by A3, XBOOLE_0:def 4;
A10: 1 <= Index p,f by A8, Th41;

now

assume A11: i1 = (Index p,f) + 1 ; :: thesis: contradiction
then (Index p,f) + (1 + 1) <= len f by A2;
then p in {(f /. ((Index p,f) + 1))} by A1, A9, A10, A11, TOPREAL1:def 8;
then p = f /. ((Index p,f) + 1) by TARSKI:def 1;
hence contradiction by A7, A6, A11, PARTFUN1:def 8; :: thesis: verum

end;

hence i1 = Index p,f by A1, A3, Th46; :: thesis: verum