let kc, km be Element of NAT ; :: thesis: for n being non zero Element of 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 Element of 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
A3: n >= 0 + 1 by NAT_1:13;
assume A4: for p being Element of (FTSL1 n) holds not f . p in U_FT p,km ; :: thesis: contradiction
A5: RelStr(# (Seg n),(Nbdl1 n) #) = FTSL1 n by FINTOPO4:def 4;
A6: FTSL1 n is filled by FINTOPO4:18;
defpred S₁[ Nat] means ( $1 > 0 & ( for j being Nat st $1 <= n & j = f . $1 holds
$1 > j ) );

now

given j being Nat such that A7: ( j = f . n & n <= j ) ; :: thesis: contradiction
A8: n in the carrier of (FTSL1 n) by A3, A5;
then f . n in the carrier of (FTSL1 n) by FUNCT_2:7;
then ( 1 <= j & j <= n ) by A5, A7, FINSEQ_1:3;
then A9: n = j by A7, XXREAL_0:1;
reconsider p2 = n as Element of (FTSL1 n) by A8;
p2 in U_FT p2 by A6, FIN_TOPO:def 4;
then A10: 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 A4, A7, A9, A10; :: thesis: verum

end;

then A11: for j being Nat st n <= n & j = f . n holds
n > j ;
then A12: 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(A12);
then consider k being Nat such that
A13: ( S₁[k] & ( for m being Nat st S₁[m] holds
k <= m ) ) ;
A14: k <= n by A11, A13;
A15: 0 + 1 <= k by A13, NAT_1:13;
then A16: k - 1 >= 0 by XREAL_1:50;
then A17: k - 1 = k -' 1 by XREAL_0:def 2;
k < k + 1 by NAT_1:13;
then A18: k - 1 < (k + 1) - 1 by XREAL_1:11;
reconsider pk = k as Element of (FTSL1 n) by A5, A14, A15, FINSEQ_1:3;

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 A13, A17, A18;

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

then A19: k - 1 = 0 by A16, XREAL_0:def 2;
1 in the carrier of (FTSL1 n) by A3, A5;
then A20: f . 1 in Seg n by A5, FUNCT_2:7;
then reconsider j0 = f . 1 as Element of NAT ;
1 > j0 by A3, A13, A19;
hence contradiction by A20, FINSEQ_1:3; :: thesis: verum

end;

suppose A21: ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ; :: thesis: contradiction

then consider j being Nat such that
A22: ( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ;
A23: k -' 1 >= 0 + 1 by A21, NAT_1:13;
then reconsider pkm = k -' 1 as Element of (FTSL1 n) by A5, A22, FINSEQ_1:3;
A24: k -' 1 in the carrier of (FTSL1 n) by A5, A22, A23;
then A25: j in the carrier of (FTSL1 n) by A22, FUNCT_2:7;

now

assume A26: k -' 1 = j ; :: thesis: contradiction
then reconsider pj = j as Element of (FTSL1 n) by A24;
pj in U_FT pj by A6, FIN_TOPO:def 4;
then A27: 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 A4, A22, A26, A27; :: thesis: verum

end;

then k -' 1 < j by A22, XXREAL_0:1;
then A28: (k -' 1) + 1 <= j by NAT_1:13;
then j - k >= 0 by A17, XREAL_1:50;
then A29: j - k = j -' k by XREAL_0:def 2;
k in NAT by ORDINAL1:def 13;
then A30: k in the carrier of (FTSL1 n) by A5, A14, A15;
then f . k in Seg n by A5, FUNCT_2:7;
then reconsider jn = f . k as Element of NAT ;
A31: Im (Nbdl1 n),k = {k,(max (k -' 1),1),(min (k + 1),n)} by A5, A30, FINTOPO4:def 3;
A32: jn < k by A13, A14;
then A33: k - jn > 0 by XREAL_1:52;
then A34: k - jn = k -' jn by XREAL_0:def 2;
not j in U_FT pkm,km by A4, A22;
then not abs ((k -' 1) - j) <= km + 1 by A5, A25, Th9;
then abs (j - (k -' 1)) > km + 1 by UNIFORM1:13;
then (j -' k) + 1 > km + 1 by A17, A29, ABSVALUE:def 1;
then A35: (j - k) + 1 >= (km + 1) + 1 by A29, NAT_1:13;
A36: jn in Seg n by A5, A30, FUNCT_2:7;
not jn in U_FT pk,km by A4;
then not abs (k - jn) <= km + 1 by A36, Th9;
then k - jn > km + 1 by A33, ABSVALUE:def 1;
then k - jn >= (km + 1) + 1 by A34, NAT_1:13;
then (k - jn) + ((j - k) + 1) >= ((km + 1) + 1) + ((km + 1) + 1) by A35, XREAL_1:9;
then (j - jn) + 1 >= (((km + 1) + 1) + (km + 1)) + 1 ;
then j - jn >= ((km + 1) + 1) + (km + 1) by XREAL_1:8;
then (j - jn) - 1 >= ((((km + 1) + 1) + km) + 1) - 1 by XREAL_1:11;
then A37: ((j - jn) - 1) / 2 >= ((2 * km) + 2) / 2 by XREAL_1:74;
[/(kc / 2)\] >= kc / 2 by INT_1:def 5;
then [/(kc / 2)\] + (2 / 2) >= (kc / 2) + (2 / 2) by XREAL_1:9;
then ((j - jn) - 1) / 2 >= (kc / 2) + (2 / 2) by A2, A37, XXREAL_0:2;
then A38: (((j - jn) - 1) / 2) * 2 >= ((kc / 2) + (2 / 2)) * 2 by XREAL_1:66;
reconsider pfk = jn as Element of (FTSL1 n) by A30, FUNCT_2:7;
A39: f .: (U_FT pk,0 ) c= U_FT pfk,kc by A1, FINTOPO4:def 2;
A40: k -' 1 in dom f by A24, FUNCT_2:def 1;
k -' 1 = max (k -' 1),1 by A23, XXREAL_0:def 10;
then k -' 1 in U_FT pk by A5, A31, ENUMSET1:def 1;
then k -' 1 in U_FT pk,0 by FINTOPO3:47;
then A41: f . (k -' 1) in f .: (U_FT pk,0 ) by A40, FUNCT_1:def 12;
jn < j by A17, A28, A32, XXREAL_0:2;
then j - jn >= 0 by XREAL_1:50;
then A42: abs (j - jn) = j - jn by ABSVALUE:def 1;
A43: abs (jn - j) = abs (j - jn) by UNIFORM1:13;
kc < kc + 2 by XREAL_1:31;
then (j - jn) - 1 > kc by A38, XXREAL_0:2;
then ((j - jn) - 1) + 1 > kc + 1 by XREAL_1:8;
hence contradiction by A22, A39, A41, A42, A43, Th9; :: thesis: verum

end;

end;