let kc, km be Nat; :: thesis: for n being non zero Nat
for f being Function of (),() st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of () st f . p in U_FT (p,km)

let n be non zero Nat; :: thesis: for f being Function of (),() st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of () st f . p in U_FT (p,km)

let f be Function of (),(); :: thesis: ( f is_continuous kc & km = [/(kc / 2)\] implies ex p being Element of () st f . p in U_FT (p,km) )
assume that
A1: f is_continuous kc and
A2: km = [/(kc / 2)\] ; :: thesis: ex p being Element of () st f . p in U_FT (p,km)
assume A3: for p being Element of () holds not f . p in U_FT (p,km) ; :: thesis: contradiction
defpred S1[ Nat] means ( \$1 > 0 & ( for j being Nat st \$1 <= n & j = f . \$1 holds
\$1 > j ) );
A4: n >= 0 + 1 by NAT_1:13;
A5: RelStr(# (Seg n),() #) = FTSL1 n by FINTOPO4:def 4;
A6: FTSL1 n is filled by FINTOPO4:18;
now :: thesis: for j being Nat holds
( not j = f . n or not n <= j )
A7: n in the carrier of () by A4, A5;
then reconsider p2 = n as Element of () ;
given j being Nat such that A8: j = f . n and
A9: n <= j ; :: thesis: contradiction
f . n in the carrier of () by ;
then j <= n by ;
then A10: n = j by ;
p2 in U_FT p2 by A6;
then A11: p2 in U_FT (p2,0) by FINTOPO3:47;
U_FT (p2,0) c= U_FT (p2,km) by ;
hence contradiction by A3, A8, A10, A11; :: thesis: verum
end;
then A12: for j being Nat st n <= n & j = f . n holds
n > j ;
then A13: ex k being Nat st S1[k] ;
ex k being Nat st
( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) ) from then consider k being Nat such that
A14: S1[k] and
A15: for m being Nat st S1[m] holds
k <= m ;
A16: 0 + 1 <= k by ;
then A17: k - 1 >= 0 by XREAL_1:48;
then A18: k - 1 = k -' 1 by XREAL_0:def 2;
k < k + 1 by NAT_1:13;
then A19: k - 1 < (k + 1) - 1 by XREAL_1:9;
A20: k <= n by ;
then reconsider pk = k as Element of () by ;
per cases ( k -' 1 <= 0 or ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) )
by ;
suppose A21: k -' 1 <= 0 ; :: thesis: contradiction
1 in the carrier of () by A4, A5;
then A22: f . 1 in Seg n by ;
then reconsider j0 = f . 1 as Nat ;
k - 1 = 0 by ;
then 1 > j0 by ;
hence contradiction by A22, FINSEQ_1:1; :: thesis: verum
end;
suppose A23: ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ; :: thesis: contradiction
A24: k in the carrier of () by A5, A20, A16;
then f . k in Seg n by ;
then reconsider jn = f . k as Nat ;
A25: not jn in U_FT (pk,km) by A3;
A26: jn < k by ;
then A27: k - jn > 0 by XREAL_1:50;
jn in Seg n by ;
then not |.(k - jn).| <= km + 1 by ;
then A28: k - jn > km + 1 by ;
k - jn = k -' jn by ;
then A29: k - jn >= (km + 1) + 1 by ;
reconsider pfk = jn as Element of () by ;
A30: kc < kc + 2 by XREAL_1:29;
A31: k -' 1 >= 0 + 1 by ;
then A32: k -' 1 = max ((k -' 1),1) by XXREAL_0:def 10;
Im ((),k) = {k,(max ((k -' 1),1)),(min ((k + 1),n))} by ;
then k -' 1 in U_FT pk by ;
then A33: k -' 1 in U_FT (pk,0) by FINTOPO3:47;
consider j being Nat such that
A34: k -' 1 <= n and
A35: j = f . (k -' 1) and
A36: k -' 1 <= j by A23;
reconsider pkm = k -' 1 as Element of () by ;
A37: not j in U_FT (pkm,km) by ;
A38: k -' 1 in the carrier of () by A5, A34, A31;
then k -' 1 in dom f by FUNCT_2:def 1;
then A39: f . (k -' 1) in f .: (U_FT (pk,0)) by ;
now :: thesis: not k -' 1 = j
assume A40: k -' 1 = j ; :: thesis: contradiction
then reconsider pj = j as Element of () by A38;
pj in U_FT pj by A6;
then A41: pj in U_FT (pj,0) by FINTOPO3:47;
U_FT (pj,0) c= U_FT (pj,km) by ;
hence contradiction by A3, A35, A40, A41; :: thesis: verum
end;
then k -' 1 < j by ;
then A42: (k -' 1) + 1 <= j by NAT_1:13;
then j - k >= 0 by ;
then A43: j - k = j -' k by XREAL_0:def 2;
j in the carrier of () by ;
then not |.((k -' 1) - j).| <= km + 1 by A5, A37, Th9;
then |.(j - (k -' 1)).| > km + 1 by UNIFORM1:11;
then (j -' k) + 1 > km + 1 by ;
then (j - k) + 1 >= (km + 1) + 1 by ;
then (k - jn) + ((j - k) + 1) >= ((km + 1) + 1) + ((km + 1) + 1) by ;
then (j - jn) + 1 >= (((km + 1) + 1) + (km + 1)) + 1 ;
then j - jn >= ((km + 1) + 1) + (km + 1) by XREAL_1:6;
then (j - jn) - 1 >= ((((km + 1) + 1) + km) + 1) - 1 by XREAL_1:9;
then A44: ((j - jn) - 1) / 2 >= ((2 * km) + 2) / 2 by XREAL_1:72;
[/(kc / 2)\] >= kc / 2 by INT_1:def 7;
then [/(kc / 2)\] + (2 / 2) >= (kc / 2) + (2 / 2) by XREAL_1:7;
then ((j - jn) - 1) / 2 >= (kc / 2) + (2 / 2) by ;
then (((j - jn) - 1) / 2) * 2 >= ((kc / 2) + (2 / 2)) * 2 by XREAL_1:64;
then (j - jn) - 1 > kc by ;
then A45: ((j - jn) - 1) + 1 > kc + 1 by XREAL_1:6;
jn < j by ;
then j - jn >= 0 by XREAL_1:48;
then A46: |.(j - jn).| = j - jn by ABSVALUE:def 1;
( f .: (U_FT (pk,0)) c= U_FT (pfk,kc) & |.(jn - j).| = |.(j - jn).| ) by ;
hence contradiction by A35, A39, A46, A45, Th9; :: thesis: verum
end;
end;