let N, M be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number 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 number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number 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:16;

now

assume A2: for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number 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 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

proof

let r be real number ; :: 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 number 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 number st
( s > 0 & Ball p,s c= f " P ) )
assume p in f " P ; :: thesis: ex s being real number st
( s > 0 & Ball p,s c= f " P )
then A4: f . p in Ball u,r by A3, FUNCT_1:def 13;
then reconsider wf = f . p as Element of M ;
P9 is open by A3, TOPMETR:21;
then consider r1 being real number such that
A5: r1 > 0 and
A6: Ball wf,r1 c= P by A3, A4, TOPMETR:22;
reconsider r1 = r1 as Real by XREAL_0:def 1;
consider s being real number 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 by XREAL_0:def 1;
Ball p,s c= f " P

proof

let x be set ; :: 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 5;
then reconsider wfx = f . wx as Element of M by TOPMETR:16;
dist p,wx < s by A9, METRIC_1:12;
then dist wf,wfx < r1 by A8;
then wfx in Ball wf,r1 by METRIC_1:12;
hence x in f " P by A1, A6, FUNCT_1:def 13; :: thesis: verum

end;

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

end;

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

end;

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

end;

hence ( ( for r being real number
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number 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