let kc, km be Nat; :: thesis: for n being non zero Nat
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)
let n be non zero Nat; :: thesis: for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)
let f be Function of (FTSL1 n),(FTSL1 n); :: thesis: ( f is_continuous kc & km = [/(kc / 2)\] implies ex p being Element of (FTSL1 n) 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 (FTSL1 n) st f . p in U_FT (p,km)
assume A3: for p being Element of (FTSL1 n) holds not f . p in U_FT (p,km) ; :: thesis: contradiction
defpred S₁[ 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),(Nbdl1 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 (FTSL1 n) by A4, A5;
then reconsider p2 = n as Element of (FTSL1 n) ;
given j being Nat such that A8: j = f . n and
A9: n <= j ; :: thesis: contradiction
f . n in the carrier of (FTSL1 n) by A7, FUNCT_2:5;
then j <= n by A5, A8, FINSEQ_1:1;
then A10: n = j by A9, XXREAL_0:1;
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 Th8, FINTOPO4:18;
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 S₁[k] ;
ex k being Nat st
( S₁[k] & ( for m being Nat st S₁[m] holds
k <= m ) ) from NAT_1:sch 5(A13);
then consider k being Nat such that
A14: S₁[k] and
A15: for m being Nat st S₁[m] holds
k <= m ;
A16: 0 + 1 <= k by A14, NAT_1:13;
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 A12, A15;
then reconsider pk = k as Element of (FTSL1 n) by A5, A16, FINSEQ_1:1;

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 A15, A18, A19;

suppose A21: k -' 1 <= 0 ; :: thesis: contradiction

1 in the carrier of (FTSL1 n) by A4, A5;
then A22: f . 1 in Seg n by A5, FUNCT_2:5;
then reconsider j0 = f . 1 as Nat ;
k - 1 = 0 by A17, A21, XREAL_0:def 2;
then 1 > j0 by A4, A14;
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 (FTSL1 n) by A5, A20, A16;
then f . k in Seg n by A5, FUNCT_2:5;
then reconsider jn = f . k as Nat ;
A25: not jn in U_FT (pk,km) by A3;
A26: jn < k by A14, A20;
then A27: k - jn > 0 by XREAL_1:50;
jn in Seg n by A5, A24, FUNCT_2:5;
then not |.(k - jn).| <= km + 1 by A25, Th9;
then A28: k - jn > km + 1 by A27, ABSVALUE:def 1;
k - jn = k -' jn by A27, XREAL_0:def 2;
then A29: k - jn >= (km + 1) + 1 by A28, NAT_1:13;
reconsider pfk = jn as Element of (FTSL1 n) by A24, FUNCT_2:5;
A30: kc < kc + 2 by XREAL_1:29;
A31: k -' 1 >= 0 + 1 by A23, NAT_1:13;
then A32: k -' 1 = max ((k -' 1),1) by XXREAL_0:def 10;
Im ((Nbdl1 n),k) = {k,(max ((k -' 1),1)),(min ((k + 1),n))} by A5, A24, FINTOPO4:def 3;
then k -' 1 in U_FT pk by A5, A32, ENUMSET1:def 1;
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 (FTSL1 n) by A5, A34, A31, FINSEQ_1:1;
A37: not j in U_FT (pkm,km) by A3, A35;
A38: k -' 1 in the carrier of (FTSL1 n) 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 A33, FUNCT_1:def 6;

now :: thesis: not k -' 1 = j

assume A40: k -' 1 = j ; :: thesis: contradiction
then reconsider pj = j as Element of (FTSL1 n) 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 Th8, FINTOPO4:18;
hence contradiction by A3, A35, A40, A41; :: thesis: verum

end;

then k -' 1 < j by A36, XXREAL_0:1;
then A42: (k -' 1) + 1 <= j by NAT_1:13;
then j - k >= 0 by A18, XREAL_1:48;
then A43: j - k = j -' k by XREAL_0:def 2;
j in the carrier of (FTSL1 n) by A35, A38, FUNCT_2:5;
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 A18, A43, ABSVALUE:def 1;
then (j - k) + 1 >= (km + 1) + 1 by A43, NAT_1:13;
then (k - jn) + ((j - k) + 1) >= ((km + 1) + 1) + ((km + 1) + 1) by A29, XREAL_1:7;
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 A2, A44, XXREAL_0:2;
then (((j - jn) - 1) / 2) * 2 >= ((kc / 2) + (2 / 2)) * 2 by XREAL_1:64;
then (j - jn) - 1 > kc by A30, XXREAL_0:2;
then A45: ((j - jn) - 1) + 1 > kc + 1 by XREAL_1:6;
jn < j by A18, A42, A26, XXREAL_0:2;
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 A1, FINTOPO4:def 2, UNIFORM1:11;
hence contradiction by A35, A39, A46, A45, Th9; :: thesis: verum

end;

end;