let N, M be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) holds
f is continuous
let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); :: thesis: ( ( for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) implies f is continuous )
dom f = the carrier of (TopSpaceMetr N) by FUNCT_2:def 1;
then A1: dom f = the carrier of N by TOPMETR:12;

now :: thesis: ( ( for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) implies f is continuous )

assume A2: for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ; :: thesis: f is continuous
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

proof

let r be Real; :: thesis: 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
let u be Element of M; :: thesis: for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open
let P be Subset of (TopSpaceMetr M); :: thesis: ( r > 0 & P = Ball (u,r) implies f " P is open )
reconsider P9 = P as Subset of (TopSpaceMetr M) ;
assume that
r > 0 and
A3: P = Ball (u,r) ; :: thesis: f " P is open
for p being Point of N st p in f " P holds
ex s being Real st
( s > 0 & Ball (p,s) c= f " P )

proof

let p be Point of N; :: thesis: ( p in f " P implies ex s being Real st
( s > 0 & Ball (p,s) c= f " P ) )
assume p in f " P ; :: thesis: ex s being Real st
( s > 0 & Ball (p,s) c= f " P )
then A4: f . p in Ball (u,r) by A3, FUNCT_1:def 7;
then reconsider wf = f . p as Element of M ;
P9 is open by A3, TOPMETR:14;
then consider r1 being Real such that
A5: r1 > 0 and
A6: Ball (wf,r1) c= P by A3, A4, TOPMETR:15;
reconsider r1 = r1 as Real ;
consider s being Real such that
A7: s > 0 and
A8: for w being Element of N
for w1 being Element of M st w1 = f . w & dist (p,w) < s holds
dist (wf,w1) < r1 by A2, A5;
reconsider s = s as Real ;
Ball (p,s) c= f " P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,s) or x in f " P )
assume A9: x in Ball (p,s) ; :: thesis: x in f " P
then reconsider wx = x as Element of N ;
f . wx in rng f by A1, FUNCT_1:def 3;
then reconsider wfx = f . wx as Element of M by TOPMETR:12;
dist (p,wx) < s by A9, METRIC_1:11;
then dist (wf,wfx) < r1 by A8;
then wfx in Ball (wf,r1) by METRIC_1:11;
hence x in f " P by A1, A6, FUNCT_1:def 7; :: thesis: verum

end;

hence ex s being Real st
( s > 0 & Ball (p,s) c= f " P ) by A7; :: thesis: verum

end;

hence f " P is open by TOPMETR:15; :: thesis: verum

end;

hence f is continuous by JORDAN2B:16; :: thesis: verum

end;

hence ( ( for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) ) implies f is continuous ) ; :: thesis: verum