let n be non zero Nat; 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); ( 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
; 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)
; contradiction
defpred S1[ 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;
now for j being Nat holds
( not j = f . n or not n <= j )end;
then A10:
for j being Nat st n <= n & j = f . n holds
n > j
;
then A11:
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 NAT_1:sch 5(A11);
then consider k being Nat such that
A12:
S1[k]
and
A13:
for m being Nat st S1[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;
now ( ( k -' 1 <= 0 & contradiction ) or ( k -' 1 > 0 & ex j being Nat st
( 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;
case A21:
(
k -' 1
> 0 & ex
j being
Nat st
(
k -' 1
<= n &
j = f . (k -' 1) &
k -' 1
<= j ) )
;
contradictionA22:
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
k -' 1
< j
by A29, XXREAL_0:1;
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 A41:
k < j
by A16, A37, XXREAL_0:1;
A44:
1
<= jn
by A23, FINSEQ_1:1;
then
jn - 1
>= 0
by XREAL_1:48;
then A45:
jn - 1
= jn -' 1
by XREAL_0:def 2;
k -' 1
in dom f
by A35, FUNCT_2:def 1;
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;
verum end;
hence
contradiction
; verum