let T be non empty TopSpace; :: thesis: for f being Function of T,R^1
for x being Point of T holds
( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
let f be Function of T,R^1; :: thesis: for x being Point of T holds
( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
let x be Point of T; :: thesis: ( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
thus ( f is_continuous_at x implies for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) ) :: thesis: ( ( for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) ) implies f is_continuous_at x )

proof

reconsider fx = f . x as Point of RealSpace by TOPMETR:16, TOPMETR:def 7;
assume A1: f is_continuous_at x ; :: thesis: for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) )
let e be real number ; :: thesis: ( e > 0 implies ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )
assume A2: e > 0 ; :: thesis: ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) )
reconsider G = Ball (fx,e) as Subset of R^1 by TOPMETR:16, TOPMETR:def 7;
( G is open & fx in G ) by A2, GOBOARD6:4, TOPMETR:21, TOPMETR:def 7;
then consider H being Subset of T such that
A3: ( H is open & x in H ) and
A4: f .: H c= G by A1, TMAP_1:48;
take H ; :: thesis: ( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) )
thus ( H is open & x in H ) by A3; :: thesis: for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e
A5: dom f = the carrier of T by FUNCT_2:def 1;
let y be Point of T; :: thesis: ( y in H implies abs ((f . y) - (f . x)) < e )
assume y in H ; :: thesis: abs ((f . y) - (f . x)) < e
then A6: f . y in f .: H by A5, FUNCT_1:def 12;
then f . y in G by A4;
then reconsider fy = f . y as Point of RealSpace ;
dist (fy,fx) < e by A4, A6, METRIC_1:12;
hence abs ((f . y) - (f . x)) < e by TOPMETR:15; :: thesis: verum

end;

assume A7: for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) ; :: thesis: f is_continuous_at x

now

reconsider fx = f . x as Point of RealSpace by TOPMETR:16, TOPMETR:def 7;
let G be Subset of R^1; :: thesis: ( G is open & f . x in G implies ex H being Subset of T st
( H is open & x in H & f .: H c= G ) )
assume ( G is open & f . x in G ) ; :: thesis: ex H being Subset of T st
( H is open & x in H & f .: H c= G )
then consider r being real number such that
A8: r > 0 and
A9: Ball (fx,r) c= G by TOPMETR:22, TOPMETR:def 7;
consider H being Subset of T such that
A10: ( H is open & x in H ) and
A11: for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < r by A7, A8;
take H = H; :: thesis: ( H is open & x in H & f .: H c= G )
thus ( H is open & x in H ) by A10; :: thesis: f .: H c= G
thus f .: H c= G :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in f .: H or a in G )
assume a in f .: H ; :: thesis: a in G
then consider y being set such that
A12: y in dom f and
A13: y in H and
A14: a = f . y by FUNCT_1:def 12;
reconsider y = y as Point of T by A12;
reconsider fy = f . y as Point of RealSpace by TOPMETR:16, TOPMETR:def 7;
abs ((f . y) - (f . x)) < r by A11, A13;
then abs (- ((f . y) - (f . x))) < r by COMPLEX1:138;
then abs ((f . x) - (f . y)) < r ;
then dist (fx,fy) < r by TOPMETR:15;
then fy in Ball (fx,r) by METRIC_1:12;
hence a in G by A9, A14; :: thesis: verum

end;

end;

hence f is_continuous_at x by TMAP_1:48; :: thesis: verum