let m be Nat; :: thesis: for T being non empty TopSpace
for f being Function of (TOP-REAL m),T holds
( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball p,s) c= V )
let T be non empty TopSpace; :: thesis: for f being Function of (TOP-REAL m),T holds
( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball p,s) c= V )
let f be Function of (TOP-REAL m),T; :: thesis: ( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball p,s) c= V )
A1: m in NAT by ORDINAL1:def 13;

hereby :: thesis: ( ( for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball p,s) c= V ) implies f is continuous )

assume A2: f is continuous ; :: thesis: for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball p,s) c= V
let p be Point of (TOP-REAL m); :: thesis: for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball p,s) c= V
let V be open Subset of T; :: thesis: ( f . p in V implies ex s being real positive number st f .: (Ball p,s) c= V )
assume f . p in V ; :: thesis: ex s being real positive number st f .: (Ball p,s) c= V
then consider W being Subset of (TOP-REAL m) such that
A3: p in W and
A4: W is open and
A5: f .: W c= V by A2, JGRAPH_2:20;
reconsider u = p as Point of (Euclid m) by EUCLID:71;
Int W = W by A4, TOPS_1:55;
then consider s being real number such that
A6: s > 0 and
A7: Ball u,s c= W by A1, A3, GOBOARD6:8;
reconsider s = s as real positive number by A6;
take s = s; :: thesis: f .: (Ball p,s) c= V
Ball u,s = Ball p,s by A1, TOPREAL9:13;
then f .: (Ball p,s) c= f .: W by A7, RELAT_1:156;
hence f .: (Ball p,s) c= V by A5, XBOOLE_1:1; :: thesis: verum

end;

assume A8: for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball p,s) c= V ; :: thesis: f is continuous
for p being Point of (TOP-REAL m)
for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TOP-REAL m) st
( p in W & W is open & f .: W c= V )

proof

let p be Point of (TOP-REAL m); :: thesis: for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TOP-REAL 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 (TOP-REAL m) st
( p in W & W is open & f .: W c= V ) )
assume that
A9: f . p in V and
A10: V is open ; :: thesis: ex W being Subset of (TOP-REAL m) st
( p in W & W is open & f .: W c= V )
consider s being real positive number such that
A11: f .: (Ball p,s) c= V by A8, A9, A10;
take W = Ball p,s; :: thesis: ( p in W & W is open & f .: W c= V )
thus p in W by A1, TOPGEN_5:17; :: thesis: ( W is open & f .: W c= V )
thus W is open ; :: thesis: f .: W c= V
thus f .: W c= V by A11; :: thesis: verum

end;

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