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_{1}[ 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;

n > j ;

then A13: ex k being Nat st S_{1}[k]
;

ex k being Nat st

( S_{1}[k] & ( for m being Nat st S_{1}[m] holds

k <= m ) ) from NAT_1:sch 5(A13);

then consider k being Nat such that

A14: S_{1}[k]
and

A15: for m being Nat st S_{1}[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;

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

$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 )

then A12:
for j being Nat st n <= n & j = f . n 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 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

n > j ;

then A13: ex k being Nat st S

ex k being Nat st

( S

k <= m ) ) from NAT_1:sch 5(A13);

then consider k being Nat such that

A14: S

A15: for m being Nat st S

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;

end;

( 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;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

suppose A23:
( k -' 1 > 0 & ex j being Nat st

( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ; :: thesis: contradiction

( 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;

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;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

then
k -' 1 < j
by A36, XXREAL_0:1;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 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

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