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

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 fx = f . x as Point of RealSpace by TOPMETR:16, TOPMETR:def 7;
reconsider G = Ball fx,e as Subset of R^1 by TOPMETR:16, TOPMETR:def 7;
A3: G is open by TOPMETR:21, TOPMETR:def 7;
fx in G by A2, GOBOARD6:4;
then consider H being Subset of T such that
A4: ( H is open & x in H & f .: H c= G ) by A1, A3, 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 A4; :: thesis: for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e
let y be Point of T; :: thesis: ( y in H implies abs ((f . y) - (f . x)) < e )
assume A5: y in H ; :: thesis: abs ((f . y) - (f . x)) < e
dom f = the carrier of T by FUNCT_2:def 1;
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

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 A8: ( 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 )
reconsider fx = f . x as Point of RealSpace by TOPMETR:16, TOPMETR:def 7;
consider r being real number such that
A9: ( r > 0 & Ball fx,r c= G ) by A8, TOPMETR:22, TOPMETR:def 7;
consider H being Subset of T such that
A10: ( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < r ) ) by A7, A9;
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
A11: ( y in dom f & y in H & a = f . y ) by FUNCT_1:def 12;
reconsider y = y as Point of T by A11;
abs ((f . y) - (f . x)) < r by A10, A11;
then abs (- ((f . y) - (f . x))) < r by COMPLEX1:138;
then A12: abs ((f . x) - (f . y)) < r ;
reconsider fy = f . y as Point of RealSpace by TOPMETR:16, TOPMETR:def 7;
dist fx,fy < r by A12, TOPMETR:15;
then fy in Ball fx,r by METRIC_1:12;
hence a in G by A9, A11; :: thesis: verum

end;

end;

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