let N, M be non empty MetrSpace; :: thesis: for f being Function of (),() 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 (),(); :: 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 () 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 () 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 () st r > 0 & P = Ball (u,r) holds
f " P is open

let u be Element of M; :: thesis: for P being Subset of () st r > 0 & P = Ball (u,r) holds
f " P is open

let P be Subset of (); :: thesis: ( r > 0 & P = Ball (u,r) implies f " P is open )
reconsider P9 = P as Subset of () ;
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 ;
then reconsider wf = f . p as Element of M ;
P9 is open by ;
then consider r1 being Real such that
A5: r1 > 0 and
A6: Ball (wf,r1) c= P by ;
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 ;
then reconsider wfx = f . wx as Element of M by TOPMETR:12;
dist (p,wx) < s by ;
then dist (wf,wfx) < r1 by A8;
then wfx in Ball (wf,r1) by METRIC_1:11;
hence x in f " P by ; :: 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