let M1, M2 be non empty MetrSpace; :: thesis: for f being Function of (),() 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 (),(); :: 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 ;
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 () 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 ;
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 ; :: thesis: verum
end;
hence f is continuous by UNIFORM1:3; :: thesis: verum