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;

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

hence
i1 = Index (p,f)
by A1, A3, Th13; :: thesis: verumassume 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;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