let n be non zero Nat; :: thesis: for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous 0 holds

ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)

let f be Function of (FTSL1 n),(FTSL1 n); :: thesis: ( f is_continuous 0 implies ex p being Element of (FTSL1 n) st f . p in U_FT (p,0) )

assume A1: f is_continuous 0 ; :: thesis: ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)

assume A2: for p being Element of (FTSL1 n) holds not f . p in U_FT (p,0) ; :: thesis: contradiction

defpred S_{1}[ Nat] means ( $1 > 0 & ( for j being Nat st $1 <= n & j = f . $1 holds

$1 > j ) );

A3: n >= 0 + 1 by NAT_1:13;

A4: RelStr(# (Seg n),(Nbdl1 n) #) = FTSL1 n by FINTOPO4:def 4;

A5: FTSL1 n is filled by FINTOPO4:18;

n > j ;

then A11: 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(A11);

then consider k being Nat such that

A12: S_{1}[k]
and

A13: for m being Nat st S_{1}[m] holds

k <= m ;

A14: 0 + 1 <= k by A12, NAT_1:13;

then A15: k - 1 >= 0 by XREAL_1:48;

then A16: k - 1 = k -' 1 by XREAL_0:def 2;

A17: k <= n by A10, A13;

then reconsider pk = k as Element of (FTSL1 n) by A4, A14, FINSEQ_1:1;

k < k + 1 by NAT_1:13;

then A18: k - 1 < (k + 1) - 1 by XREAL_1:9;

ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)

let f be Function of (FTSL1 n),(FTSL1 n); :: thesis: ( f is_continuous 0 implies ex p being Element of (FTSL1 n) st f . p in U_FT (p,0) )

assume A1: f is_continuous 0 ; :: thesis: ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)

assume A2: for p being Element of (FTSL1 n) holds not f . p in U_FT (p,0) ; :: thesis: contradiction

defpred S

$1 > j ) );

A3: n >= 0 + 1 by NAT_1:13;

A4: RelStr(# (Seg n),(Nbdl1 n) #) = FTSL1 n by FINTOPO4:def 4;

A5: FTSL1 n is filled by FINTOPO4:18;

now :: thesis: for j being Nat holds

( not j = f . n or not n <= j )

then A10:
for j being Nat st n <= n & j = f . n holds ( not j = f . n or not n <= j )

A6:
n in the carrier of (FTSL1 n)
by A3, A4;

then reconsider p2 = n as Element of (FTSL1 n) ;

p2 in U_FT p2 by A5;

then A7: p2 in U_FT (p2,0) by FINTOPO3:47;

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 A6, FUNCT_2:5;

then j <= n by A4, A8, FINSEQ_1:1;

then n = j by A9, XXREAL_0:1;

hence contradiction by A2, A8, A7; :: thesis: verum

end;then reconsider p2 = n as Element of (FTSL1 n) ;

p2 in U_FT p2 by A5;

then A7: p2 in U_FT (p2,0) by FINTOPO3:47;

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 A6, FUNCT_2:5;

then j <= n by A4, A8, FINSEQ_1:1;

then n = j by A9, XXREAL_0:1;

hence contradiction by A2, A8, A7; :: thesis: verum

n > j ;

then A11: ex k being Nat st S

ex k being Nat st

( S

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

then consider k being Nat such that

A12: S

A13: for m being Nat st S

k <= m ;

A14: 0 + 1 <= k by A12, NAT_1:13;

then A15: k - 1 >= 0 by XREAL_1:48;

then A16: k - 1 = k -' 1 by XREAL_0:def 2;

A17: k <= n by A10, A13;

then reconsider pk = k as Element of (FTSL1 n) by A4, A14, FINSEQ_1:1;

k < k + 1 by NAT_1:13;

then A18: k - 1 < (k + 1) - 1 by XREAL_1:9;

now :: thesis: ( ( k -' 1 <= 0 & contradiction ) or ( k -' 1 > 0 & ex j being Nat st

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

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

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, A16, A18;

end;

( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ) by A13, A16, A18;

case A19:
k -' 1 <= 0
; :: thesis: contradiction

1 in the carrier of (FTSL1 n)
by A3, A4;

then A20: f . 1 in Seg n by A4, FUNCT_2:5;

then reconsider j0 = f . 1 as Nat ;

k - 1 = 0 by A15, A19, XREAL_0:def 2;

then 1 > j0 by A3, A12;

hence contradiction by A20, FINSEQ_1:1; :: thesis: verum

end;then A20: f . 1 in Seg n by A4, FUNCT_2:5;

then reconsider j0 = f . 1 as Nat ;

k - 1 = 0 by A15, A19, XREAL_0:def 2;

then 1 > j0 by A3, A12;

hence contradiction by A20, FINSEQ_1:1; :: thesis: verum

case A21:
( 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

A22:
k in the carrier of (FTSL1 n)
by A4, A17, A14;

then A23: f . k in Seg n by A4, FUNCT_2:5;

then reconsider jn = f . k as Nat ;

jn < jn + 1 by NAT_1:13;

then A24: jn - 1 < (jn + 1) - 1 by XREAL_1:9;

A25: k -' 1 >= 0 + 1 by A21, NAT_1:13;

then A26: ( k -' 1 = k or k -' 1 = max ((k -' 1),1) or k -' 1 = min ((k + 1),n) ) by XXREAL_0:def 10;

consider j being Nat such that

A27: k -' 1 <= n and

A28: j = f . (k -' 1) and

A29: k -' 1 <= j by A21;

reconsider pkm = k -' 1 as Element of (FTSL1 n) by A4, A27, A25, FINSEQ_1:1;

k -' 1 in Seg n by A27, A25;

then A30: Im ((Nbdl1 n),pkm) = {(k -' 1),(max (((k -' 1) -' 1),1)),(min (((k -' 1) + 1),n))} by FINTOPO4:def 3;

Im ((Nbdl1 n),k) = {k,(max ((k -' 1),1)),(min ((k + 1),n))} by A4, A22, FINTOPO4:def 3;

then k -' 1 in U_FT pk by A4, A26, ENUMSET1:def 1;

then A31: k -' 1 in U_FT (pk,0) by FINTOPO3:47;

reconsider pfk = jn as Element of (FTSL1 n) by A22, FUNCT_2:5;

A32: f .: (U_FT (pk,0)) c= U_FT (pfk,0) by A1, FINTOPO4:def 2;

A33: jn < k by A12, A17;

then A34: jn + 1 <= k by NAT_1:13;

A35: k -' 1 in the carrier of (FTSL1 n) by A4, A27, A25;

then A37: (k -' 1) + 1 <= j by NAT_1:13;

then A38: jn < j by A16, A33, XXREAL_0:2;

j in the carrier of (FTSL1 n) by A28, A35, FUNCT_2:5;

then A39: j <= n by A4, FINSEQ_1:1;

then jn - 1 >= 0 by XREAL_1:48;

then A45: jn - 1 = jn -' 1 by XREAL_0:def 2;

then f . (k -' 1) in f .: (U_FT (pk,0)) by A31, FUNCT_1:def 6;

then A47: j in U_FT (pfk,0) by A28, A32;

Im ((Nbdl1 n),jn) = {jn,(max ((jn -' 1),1)),(min ((jn + 1),n))} by A23, FINTOPO4:def 3;

then not j in U_FT pfk by A4, A16, A37, A33, A46, A42, ENUMSET1:def 1;

hence contradiction by A47, FINTOPO3:47; :: thesis: verum

end;then A23: f . k in Seg n by A4, FUNCT_2:5;

then reconsider jn = f . k as Nat ;

jn < jn + 1 by NAT_1:13;

then A24: jn - 1 < (jn + 1) - 1 by XREAL_1:9;

A25: k -' 1 >= 0 + 1 by A21, NAT_1:13;

then A26: ( k -' 1 = k or k -' 1 = max ((k -' 1),1) or k -' 1 = min ((k + 1),n) ) by XXREAL_0:def 10;

consider j being Nat such that

A27: k -' 1 <= n and

A28: j = f . (k -' 1) and

A29: k -' 1 <= j by A21;

reconsider pkm = k -' 1 as Element of (FTSL1 n) by A4, A27, A25, FINSEQ_1:1;

k -' 1 in Seg n by A27, A25;

then A30: Im ((Nbdl1 n),pkm) = {(k -' 1),(max (((k -' 1) -' 1),1)),(min (((k -' 1) + 1),n))} by FINTOPO4:def 3;

Im ((Nbdl1 n),k) = {k,(max ((k -' 1),1)),(min ((k + 1),n))} by A4, A22, FINTOPO4:def 3;

then k -' 1 in U_FT pk by A4, A26, ENUMSET1:def 1;

then A31: k -' 1 in U_FT (pk,0) by FINTOPO3:47;

reconsider pfk = jn as Element of (FTSL1 n) by A22, FUNCT_2:5;

A32: f .: (U_FT (pk,0)) c= U_FT (pfk,0) by A1, FINTOPO4:def 2;

A33: jn < k by A12, A17;

then A34: jn + 1 <= k by NAT_1:13;

A35: k -' 1 in the carrier of (FTSL1 n) by A4, A27, A25;

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

then
k -' 1 < j
by A29, XXREAL_0:1;assume A36:
k -' 1 = j
; :: thesis: contradiction

then reconsider pj = j as Element of (FTSL1 n) by A35;

pj in U_FT pj by A5;

then f . j in U_FT (pj,0) by A28, A36, FINTOPO3:47;

hence contradiction by A2; :: thesis: verum

end;then reconsider pj = j as Element of (FTSL1 n) by A35;

pj in U_FT pj by A5;

then f . j in U_FT (pj,0) by A28, A36, FINTOPO3:47;

hence contradiction by A2; :: thesis: verum

then A37: (k -' 1) + 1 <= j by NAT_1:13;

then A38: jn < j by A16, A33, XXREAL_0:2;

j in the carrier of (FTSL1 n) by A28, A35, FUNCT_2:5;

then A39: j <= n by A4, FINSEQ_1:1;

now :: thesis: not k = j

then A41:
k < j
by A16, A37, XXREAL_0:1;assume A40:
k = j
; :: thesis: contradiction

then min (((k -' 1) + 1),n) = (k -' 1) + 1 by A16, A39, XXREAL_0:def 9;

then k in U_FT pkm by A4, A16, A30, ENUMSET1:def 1;

then f . (k -' 1) in U_FT (pkm,0) by A28, A40, FINTOPO3:47;

hence contradiction by A2; :: thesis: verum

end;then min (((k -' 1) + 1),n) = (k -' 1) + 1 by A16, A39, XXREAL_0:def 9;

then k in U_FT pkm by A4, A16, A30, ENUMSET1:def 1;

then f . (k -' 1) in U_FT (pkm,0) by A28, A40, FINTOPO3:47;

hence contradiction by A2; :: thesis: verum

A42: now :: thesis: ( ( jn + 1 <= n & j <> min ((jn + 1),n) ) or ( jn + 1 > n & j <> min ((jn + 1),n) ) )

A44:
1 <= jn
by A23, FINSEQ_1:1;end;

then jn - 1 >= 0 by XREAL_1:48;

then A45: jn - 1 = jn -' 1 by XREAL_0:def 2;

A46: now :: thesis: j <> max ((jn -' 1),1)

k -' 1 in dom f
by A35, FUNCT_2:def 1;end;

then f . (k -' 1) in f .: (U_FT (pk,0)) by A31, FUNCT_1:def 6;

then A47: j in U_FT (pfk,0) by A28, A32;

Im ((Nbdl1 n),jn) = {jn,(max ((jn -' 1),1)),(min ((jn + 1),n))} by A23, FINTOPO4:def 3;

then not j in U_FT pfk by A4, A16, A37, A33, A46, A42, ENUMSET1:def 1;

hence contradiction by A47, FINTOPO3:47; :: thesis: verum