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
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 ) holds
f is continuous
let M be non empty MetrSpace; :: thesis: for f being Function of X,(TopSpaceMetr M) st ( for r being Real
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 ) holds
f is continuous
let f be Function of X,(TopSpaceMetr M); :: thesis: ( ( for r being Real
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 ) implies f is continuous )
assume A1: for r being Real
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: 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 :: thesis: ( x in f " P1 implies ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) )

assume A4: x in f " P1 ; :: thesis: ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q )
then A5: x in dom f by FUNCT_1:def 7;
A6: f . x in P1 by A4, FUNCT_1:def 7;
then reconsider u = f . x as Element of M by TOPMETR:12;
consider r being Real such that
A7: r > 0 and
A8: Ball (u,r) c= P1 by A3, A6, TOPMETR:15;
reconsider r = r as Real ;
reconsider PB = Ball (u,r) as Subset of (TopSpaceMetr M) by TOPMETR:12;
A9: f " PB c= f " P1 by A8, RELAT_1:143;
f . x in Ball (u,r) by A7, TBSP_1:11;
then x in f " (Ball (u,r)) by A5, FUNCT_1:def 7;
hence ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) by A1, A7, A9; :: 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:25; :: thesis: verum

end;

[#] (TopSpaceMetr M) <> {} ;
hence f is continuous by A2, TOPS_2:43; :: thesis: verum