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;

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

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 )

hence
( ( for r being Realfor 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

end;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

hence
f is continuous
by JORDAN2B:16; :: thesis: verum
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 )

end;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

hence
f " P is open
by TOPMETR:15; :: thesis: verum
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

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

end;( 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

hence
ex s being Real st
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;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

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

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