let n be non zero Nat; :: thesis: for f being Function of (),() st f is_continuous 0 holds
ex p being Element of () st f . p in U_FT (p,0)

let f be Function of (),(); :: thesis: ( f is_continuous 0 implies ex p being Element of () st f . p in U_FT (p,0) )
assume A1: f is_continuous 0 ; :: thesis: ex p being Element of () st f . p in U_FT (p,0)
assume A2: for p being Element of () holds not f . p in U_FT (p,0) ; :: thesis: 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),() #) = 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 )
A6: n in the carrier of () by A3, A4;
then reconsider p2 = n as Element of () ;
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 () by ;
then j <= n by ;
then n = j by ;
hence contradiction by A2, A8, A7; :: thesis: verum
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 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 ;
then A15: k - 1 >= 0 by XREAL_1:48;
then A16: k - 1 = k -' 1 by XREAL_0:def 2;
A17: k <= n by ;
then reconsider pk = k as Element of () by ;
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 ) )
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 ;
case A19: k -' 1 <= 0 ; :: thesis: contradiction
1 in the carrier of () by A3, A4;
then A20: f . 1 in Seg n by ;
then reconsider j0 = f . 1 as Nat ;
k - 1 = 0 by ;
then 1 > j0 by ;
hence contradiction by A20, FINSEQ_1:1; :: thesis: verum
end;
case A21: ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ; :: thesis: contradiction
A22: k in the carrier of () by A4, A17, A14;
then A23: f . k in Seg n by ;
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 ;
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 () by ;
k -' 1 in Seg n by ;
then A30: Im ((),pkm) = {(k -' 1),(max (((k -' 1) -' 1),1)),(min (((k -' 1) + 1),n))} by FINTOPO4:def 3;
Im ((),k) = {k,(max ((k -' 1),1)),(min ((k + 1),n))} by ;
then k -' 1 in U_FT pk by ;
then A31: k -' 1 in U_FT (pk,0) by FINTOPO3:47;
reconsider pfk = jn as Element of () by ;
A32: f .: (U_FT (pk,0)) c= U_FT (pfk,0) by ;
A33: jn < k by ;
then A34: jn + 1 <= k by NAT_1:13;
A35: k -' 1 in the carrier of () by A4, A27, A25;
now :: thesis: not k -' 1 = j
assume A36: k -' 1 = j ; :: thesis: contradiction
then reconsider pj = j as Element of () by A35;
pj in U_FT pj by A5;
then f . j in U_FT (pj,0) by ;
hence contradiction by A2; :: thesis: verum
end;
then k -' 1 < j by ;
then A37: (k -' 1) + 1 <= j by NAT_1:13;
then A38: jn < j by ;
j in the carrier of () by ;
then A39: j <= n by ;
now :: thesis: not k = j
assume A40: k = j ; :: thesis: contradiction
then min (((k -' 1) + 1),n) = (k -' 1) + 1 by ;
then k in U_FT pkm by ;
then f . (k -' 1) in U_FT (pkm,0) by ;
hence contradiction by A2; :: thesis: verum
end;
then A41: k < j by ;
A42: now :: thesis: ( ( jn + 1 <= n & j <> min ((jn + 1),n) ) or ( jn + 1 > n & j <> min ((jn + 1),n) ) )
per cases ( jn + 1 <= n or jn + 1 > n ) ;
case jn + 1 <= n ; :: thesis: j <> min ((jn + 1),n)
hence j <> min ((jn + 1),n) by ; :: thesis: verum
end;
case A43: jn + 1 > n ; :: thesis: j <> min ((jn + 1),n)
then jn >= n by NAT_1:13;
hence j <> min ((jn + 1),n) by ; :: thesis: verum
end;
end;
end;
A44: 1 <= jn by ;
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)
per cases ( jn -' 1 >= 1 or jn -' 1 < 1 ) ;
suppose jn -' 1 >= 1 ; :: thesis: j <> max ((jn -' 1),1)
hence j <> max ((jn -' 1),1) by ; :: thesis: verum
end;
suppose jn -' 1 < 1 ; :: thesis: j <> max ((jn -' 1),1)
hence j <> max ((jn -' 1),1) by ; :: thesis: verum
end;
end;
end;
k -' 1 in dom f by ;
then f . (k -' 1) in f .: (U_FT (pk,0)) by ;
then A47: j in U_FT (pfk,0) by ;
Im ((),jn) = {jn,(max ((jn -' 1),1)),(min ((jn + 1),n))} by ;
then not j in U_FT pfk by ;
hence contradiction by A47, FINTOPO3:47; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum