let n be non zero Element of 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
A2:
n >= 0 + 1
by NAT_1:13;
assume A3:
for p being Element of (FTSL1 n) holds not f . p in U_FT p,0
; :: thesis: contradiction
A4:
RelStr(# (Seg n),(Nbdl1 n) #) = FTSL1 n
by FINTOPO4:def 4;
A5:
FTSL1 n is filled
by FINTOPO4:18;
defpred S1[ Nat] means ( $1 > 0 & ( for j being Nat st $1 <= n & j = f . $1 holds
$1 > j ) );
then A9:
for j being Nat st n <= n & j = f . n holds
n > j
;
then A10:
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(A10);
then consider k being Nat such that
A11:
( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) )
;
A12:
k <= n
by A9, A11;
A13:
0 + 1 <= k
by A11, NAT_1:13;
then A14:
k - 1 >= 0
by XREAL_1:50;
then A15:
k - 1 = k -' 1
by XREAL_0:def 2;
k < k + 1
by NAT_1:13;
then A16:
k - 1 < (k + 1) - 1
by XREAL_1:11;
reconsider pk = k as Element of (FTSL1 n) by A4, A12, A13, FINSEQ_1:3;
now 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 A11, A15, A16;
case A19:
(
k -' 1
> 0 & ex
j being
Nat st
(
k -' 1
<= n &
j = f . (k -' 1) &
k -' 1
<= j ) )
;
:: thesis: contradictionthen consider j being
Nat such that A20:
(
k -' 1
<= n &
j = f . (k -' 1) &
k -' 1
<= j )
;
A21:
k -' 1
>= 0 + 1
by A19, NAT_1:13;
then A22:
k -' 1
in the
carrier of
(FTSL1 n)
by A4, A20;
then
j in the
carrier of
(FTSL1 n)
by A20, FUNCT_2:7;
then A23:
( 1
<= j &
j <= n )
by A4, FINSEQ_1:3;
then
k -' 1
< j
by A20, XXREAL_0:1;
then A25:
(k -' 1) + 1
<= j
by NAT_1:13;
reconsider pkm =
k -' 1 as
Element of
(FTSL1 n) by A4, A20, A21, FINSEQ_1:3;
k -' 1
in Seg n
by A20, A21;
then A26:
Im (Nbdl1 n),
pkm = {(k -' 1),(max ((k -' 1) -' 1),1),(min ((k -' 1) + 1),n)}
by FINTOPO4:def 3;
then A28:
k < j
by A15, A25, XXREAL_0:1;
k in NAT
by ORDINAL1:def 13;
then A29:
k in the
carrier of
(FTSL1 n)
by A4, A12, A13;
then A30:
f . k in Seg n
by A4, FUNCT_2:7;
then reconsider jn =
f . k as
Element of
NAT ;
A31:
Im (Nbdl1 n),
jn = {jn,(max (jn -' 1),1),(min (jn + 1),n)}
by A30, FINTOPO4:def 3;
A32:
Im (Nbdl1 n),
k = {k,(max (k -' 1),1),(min (k + 1),n)}
by A4, A29, FINTOPO4:def 3;
A33:
( 1
<= jn &
jn <= n )
by A30, FINSEQ_1:3;
A34:
jn < k
by A11, A12;
then A35:
jn + 1
<= k
by NAT_1:13;
reconsider pfk =
jn as
Element of
(FTSL1 n) by A29, FUNCT_2:7;
A36:
f .: (U_FT pk,0 ) c= U_FT pfk,
0
by A1, FINTOPO4:def 2;
A37:
k -' 1
in dom f
by A22, FUNCT_2:def 1;
(
k -' 1
= k or
k -' 1
= max (k -' 1),1 or
k -' 1
= min (k + 1),
n )
by A21, XXREAL_0:def 10;
then
k -' 1
in U_FT pk
by A4, A32, ENUMSET1:def 1;
then
k -' 1
in U_FT pk,
0
by FINTOPO3:47;
then
f . (k -' 1) in f .: (U_FT pk,0 )
by A37, FUNCT_1:def 12;
then A38:
j in U_FT pfk,
0
by A20, A36;
A39:
jn < j
by A15, A25, A34, XXREAL_0:2;
jn - 1
>= 0
by A33, XREAL_1:50;
then A40:
jn - 1
= jn -' 1
by XREAL_0:def 2;
jn < jn + 1
by NAT_1:13;
then A41:
jn - 1
< (jn + 1) - 1
by XREAL_1:11;
then
not
j in U_FT pfk
by A4, A15, A25, A31, A34, A42, ENUMSET1:def 1;
hence
contradiction
by A38, FINTOPO3:47;
:: thesis: verum end;
hence
contradiction
; :: thesis: verum