let S be non empty TopSpace; :: thesis:
let T be non empty MetrSpace; :: thesis:
let f be Function of S,(TopSpaceMetr T); :: thesis:
let x be Point of S; :: thesis:

hereby :: thesis:

assume A1: f is_continuous_at x ; :: thesis:
let e be Real; :: thesis:
assume A2: 0 < e ; :: thesis:
reconsider V = Ball ((In ((f . x),T)),e) as Subset of (TopSpaceMetr T) ;
dist ((In ((f . x),T)),(In ((f . x),T))) = 0 by METRIC_1:1;
then In ((f . x),T) in V by METRIC_1:11, A2;
then consider H being Subset of S such that
A3: ( H is open & x in H & f .: H c= V ) by A1, TMAP_1:43, TOPMETR:14;
take H = H; :: thesis:
thus H is open by A3; :: thesis:
thus x in H by A3; :: thesis:
let y be Point of S; :: thesis:
assume y in H ; :: thesis:
then f . y in f .: H by FUNCT_2:35;
hence dist ((In ((f . x),T)),(In ((f . y),T))) < e by A3, METRIC_1:11; :: thesis:

end;

assume A4: for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((f . x),T)),(In ((f . y),T))) < e ) ) ; :: thesis:
for G being Subset of (TopSpaceMetr T) st G is open & f . x in G holds
ex H being Subset of S st
( H is open & x in H & f .: H c= G )

proof

let G be Subset of (TopSpaceMetr T); :: thesis:
assume ( G is open & f . x in G ) ; :: thesis:
then consider r being Real such that
A5: ( r > 0 & Ball ((In ((f . x),T)),r) c= G ) by TOPMETR:15;
consider H being Subset of S such that
A6: ( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((f . x),T)),(In ((f . y),T))) < r ) ) by A4, A5;
take H ; :: thesis:
thus H is open by A6; :: thesis:
thus x in H by A6; :: thesis:

now :: thesis:

let z be object ; :: thesis:
assume z in f .: H ; :: thesis:
then consider t being object such that
A7: ( t in dom f & t in H & z = f . t ) by FUNCT_1:def 6;
reconsider t = t as Point of S by A7;
dist ((In ((f . x),T)),(In ((f . t),T))) < r by A7, A6;
hence z in G by A5, A7, METRIC_1:11; :: thesis:

end;

hence f .: H c= G ; :: thesis:

end;

hence f is_continuous_at x by TMAP_1:43; :: thesis: