let p be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2) st len f >= 2 & not p in L~ f holds

for n being Nat st 1 <= n & n <= len f holds

f /. n <> p

let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f >= 2 & not p in L~ f implies for n being Nat st 1 <= n & n <= len f holds

f /. n <> p )

assume that

A1: len f >= 2 and

A2: not p in L~ f ; :: thesis: for n being Nat st 1 <= n & n <= len f holds

f /. n <> p

set Mf = { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } ;

given n being Nat such that A3: 1 <= n and

A4: n <= len f and

A5: f /. n = p ; :: thesis: contradiction

for n being Nat st 1 <= n & n <= len f holds

f /. n <> p

let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f >= 2 & not p in L~ f implies for n being Nat st 1 <= n & n <= len f holds

f /. n <> p )

assume that

A1: len f >= 2 and

A2: not p in L~ f ; :: thesis: for n being Nat st 1 <= n & n <= len f holds

f /. n <> p

set Mf = { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } ;

given n being Nat such that A3: 1 <= n and

A4: n <= len f and

A5: f /. n = p ; :: thesis: contradiction

per cases
( n = len f or n < len f )
by A4, XXREAL_0:1;

end;

suppose A6:
n = len f
; :: thesis: contradiction

reconsider j = (len f) - 1 as Element of NAT by A1, INT_1:5, XXREAL_0:2;

1 + 1 <= len f by A1;

then A7: 1 <= j by XREAL_1:19;

then A8: f /. (j + 1) in LSeg (f,j) by TOPREAL1:21;

j + 1 <= len f ;

then LSeg (f,j) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A7;

hence contradiction by A2, A5, A6, A8, TARSKI:def 4; :: thesis: verum

end;1 + 1 <= len f by A1;

then A7: 1 <= j by XREAL_1:19;

then A8: f /. (j + 1) in LSeg (f,j) by TOPREAL1:21;

j + 1 <= len f ;

then LSeg (f,j) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A7;

hence contradiction by A2, A5, A6, A8, TARSKI:def 4; :: thesis: verum

suppose A9:
n < len f
; :: thesis: contradiction

then
n + 1 <= len f
by NAT_1:13;

then A10: f /. n in LSeg (f,n) by A3, TOPREAL1:21;

n + 1 <= len f by A9, NAT_1:13;

then LSeg (f,n) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A3;

hence contradiction by A2, A5, A10, TARSKI:def 4; :: thesis: verum

end;then A10: f /. n in LSeg (f,n) by A3, TOPREAL1:21;

n + 1 <= len f by A9, NAT_1:13;

then LSeg (f,n) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A3;

hence contradiction by A2, A5, A10, TARSKI:def 4; :: thesis: verum