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, Th7;
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:25;
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 Th9;
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, Th8;
now :: thesis: not i1 = (Index (p,f)) + 1
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 6;
then p = f /. ((Index (p,f)) + 1) by TARSKI:def 1;
hence contradiction by A7, A6, A11, PARTFUN1:def 6; :: thesis: verum
end;
hence i1 = Index (p,f) by A1, A3, Th13; :: thesis: verum