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 positive Real st q = f . p holds
ex s being positive Real 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 positive Real st q = f . p holds
ex s being positive Real 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 positive Real st q = f . p holds
ex s being positive Real 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 positive Real st q = f . p holds
ex s being positive Real 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 positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)
let q be Point of M2; :: thesis: for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)
let r be positive Real; :: thesis: ( q = f . p implies ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )
assume A2: q = f . p ; :: thesis: ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)
consider s being 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:4;
reconsider s = s as positive Real 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 object ; :: 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:65;
reconsider x1 = x as Point of M1 ;
reconsider y1 = y as Point of M2 by A6;
dist (p,x1) < s by A5, METRIC_1:11;
then dist (q,y1) < r by A6, A4;
hence y in Ball (q,r) by METRIC_1:11; :: thesis: verum

end;

end;

assume A7: for p being Point of M1
for q being Point of M2
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) ; :: thesis: f is continuous
for r being Real
for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being Real 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; :: thesis: for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being Real 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 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 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 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 positive Real 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:11;
then f . w in f .: (Ball (u,s)) by FUNCT_2:35;
hence dist (u1,w1) < r by A8, A9, METRIC_1:11; :: thesis: verum

end;

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