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

end;

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

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

end;