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
per cases ( n = len f or n < len f ) by A4, XXREAL_0:1;
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;
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;
end;