let f be FinSequence of (); :: thesis: for p being Point of ()
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 (); :: 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 ;
A5: 1 <= (Index (p,f)) + 1 by NAT_1:11;
Index (p,f) <= i1 by ;
then Index (p,f) < len f by ;
then (Index (p,f)) + 1 <= len f by NAT_1:13;
then A6: (Index (p,f)) + 1 in dom f by ;
assume A7: p <> f . i1 ; :: thesis: i1 = Index (p,f)
A8: p in L~ f by ;
then p in LSeg (f,(Index (p,f))) by Th9;
then A9: p in (LSeg (f,(Index (p,f)))) /\ (LSeg (f,i1)) by ;
A10: 1 <= Index (p,f) by ;
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 ;
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