let X be non empty TopSpace; :: thesis: for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st ( for r being real number
for u being Element of the carrier of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball u,r holds
f " P is open ) holds
f is continuous
let M be non empty MetrSpace; :: thesis: for f being Function of X,(TopSpaceMetr M) st ( for r being real number
for u being Element of the carrier of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball u,r holds
f " P is open ) holds
f is continuous
let f be Function of X,(TopSpaceMetr M); :: thesis: ( ( for r being real number
for u being Element of the carrier of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball u,r holds
f " P is open ) implies f is continuous )
assume A1: for r being real number
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball u,r holds
f " P is open ; :: thesis: f is continuous
A2: [#] (TopSpaceMetr M) <> {} ;
for P1 being Subset of (TopSpaceMetr M) st P1 is open holds
f " P1 is open

proof

let P1 be Subset of (TopSpaceMetr M); :: thesis: ( P1 is open implies f " P1 is open )
assume A3: P1 is open ; :: thesis: f " P1 is open
for x being set holds
( x in f " P1 iff ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) )

proof

let x be set ; :: thesis: ( x in f " P1 iff ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) )

now

assume x in f " P1 ; :: thesis: ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q )
then A4: ( x in dom f & f . x in P1 ) by FUNCT_1:def 13;
then reconsider u = f . x as Element of M by TOPMETR:16;
consider r being real number such that
A5: ( r > 0 & Ball u,r c= P1 ) by A3, A4, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
reconsider PB = Ball u,r as Subset of (TopSpaceMetr M) by TOPMETR:16;
A6: f " PB c= f " P1 by A5, RELAT_1:178;
f . x in Ball u,r by A5, TBSP_1:16;
then x in f " (Ball u,r) by A4, FUNCT_1:def 13;
hence ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) by A1, A5, A6; :: thesis: verum

end;

hence ( x in f " P1 iff ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) ) ; :: thesis: verum

end;

hence f " P1 is open by TOPS_1:57; :: thesis: verum

end;

hence f is continuous by A2, TOPS_2:55; :: thesis: verum