let M1, M2 be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is continuous iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball p,s) c= Ball q,r )
let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); :: thesis: ( f is continuous iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball p,s) c= Ball q,r )

hereby :: thesis: ( ( for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball p,s) c= Ball q,r ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball p,s) c= Ball q,r
let p be Point of M1; :: thesis: for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball p,s) c= Ball q,r
let q be Point of M2; :: thesis: for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball p,s) c= Ball q,r
let r be real positive number ; :: thesis: ( q = f . p implies ex s being real positive number st f .: (Ball p,s) c= Ball q,r )
assume A2: q = f . p ; :: thesis: ex s being real positive number st f .: (Ball p,s) c= Ball q,r
r in REAL by XREAL_0:def 1;
then consider s being Element of REAL such that
A3: s > 0 and
A4: for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist p,w < s holds
dist q,w1 < r by A1, A2, UNIFORM1:5;
reconsider s = s as real positive number by A3;
take s = s; :: thesis: f .: (Ball p,s) c= Ball q,r
thus f .: (Ball p,s) c= Ball q,r :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Ball p,s) or y in Ball q,r )
assume y in f .: (Ball p,s) ; :: thesis: y in Ball q,r
then consider x being Point of (TopSpaceMetr M1) such that
A5: x in Ball p,s and
A6: f . x = y by FUNCT_2:116;
reconsider x1 = x as Point of M1 ;
reconsider y1 = y as Point of M2 by A6;
dist p,x1 < s by A5, METRIC_1:12;
then dist q,y1 < r by A6, A4;
hence y in Ball q,r by METRIC_1:12; :: thesis: verum

end;

end;

assume A7: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball p,s) c= Ball q,r ; :: thesis: f is continuous
for r being real number
for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) )

proof

let r be real number ; :: thesis: for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) )
let u be Element of M1; :: thesis: for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) )
let u1 be Element of M2; :: thesis: ( r > 0 & u1 = f . u implies ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) ) )
assume ( r > 0 & u1 = f . u ) ; :: thesis: ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) )
then consider s being real positive number such that
A8: f .: (Ball u,s) c= Ball u1,r by A7;
take s ; :: thesis: ( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) )
thus s > 0 ; :: thesis: for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r
let w be Element of M1; :: thesis: for w1 being Element of M2 st w1 = f . w & dist u,w < s holds
dist u1,w1 < r
let w1 be Element of M2; :: thesis: ( w1 = f . w & dist u,w < s implies dist u1,w1 < r )
assume A9: w1 = f . w ; :: thesis: ( not dist u,w < s or dist u1,w1 < r )
assume dist u,w < s ; :: thesis: dist u1,w1 < r
then w in Ball u,s by METRIC_1:12;
then f . w in f .: (Ball u,s) by FUNCT_2:43;
hence dist u1,w1 < r by A8, A9, METRIC_1:12; :: thesis: verum

end;

hence f is continuous by UNIFORM1:4; :: thesis: verum