let T be non empty TopSpace; :: thesis: for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V )
let M be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V )
let f be Function of (TopSpaceMetr M),T; :: thesis: ( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V )

hereby :: thesis: ( ( for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V
let p be Point of M; :: thesis: for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V
let V be open Subset of T; :: thesis: ( f . p in V implies ex s being positive Real st f .: (Ball (p,s)) c= V )
assume f . p in V ; :: thesis: ex s being positive Real st f .: (Ball (p,s)) c= V
then consider W being Subset of (TopSpaceMetr M) such that
A2: p in W and
A3: W is open and
A4: f .: W c= V by A1, JGRAPH_2:10;
Int W = W by A3, TOPS_1:23;
then consider s being Real such that
A5: s > 0 and
A6: Ball (p,s) c= W by A2, GOBOARD6:4;
reconsider s = s as positive Real by A5;
take s = s; :: thesis: f .: (Ball (p,s)) c= V
f .: (Ball (p,s)) c= f .: W by A6, RELAT_1:123;
hence f .: (Ball (p,s)) c= V by A4; :: thesis: verum

end;

assume A7: for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V ; :: thesis: f is continuous
for p being Point of (TopSpaceMetr M)
for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V )

proof

let p be Point of (TopSpaceMetr M); :: thesis: for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V )
let V be Subset of T; :: thesis: ( f . p in V & V is open implies ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V ) )
assume that
A8: f . p in V and
A9: V is open ; :: thesis: ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V )
reconsider u = p as Point of M ;
consider s being positive Real such that
A10: f .: (Ball (u,s)) c= V by A7, A8, A9;
reconsider W = Ball (u,s) as Subset of (TopSpaceMetr M) ;
take W ; :: thesis: ( p in W & W is open & f .: W c= V )
thus p in W by GOBOARD6:1; :: thesis: ( W is open & f .: W c= V )
thus W is open by TOPMETR:14; :: thesis: f .: W c= V
thus f .: W c= V by A10; :: thesis: verum

end;

hence f is continuous by JGRAPH_2:10; :: thesis: verum