let n, m be Nat; :: thesis: for f being Function of (),() holds
( f is continuous iff for p being Point of ()
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) )

let f be Function of (),(); :: thesis: ( f is continuous iff for p being Point of ()
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) )

A1: ( TopStruct(# the U1 of (), the topology of () #) = TopSpaceMetr () & TopStruct(# the U1 of (), the topology of () #) = TopSpaceMetr () ) by EUCLID:def 8;
then reconsider f1 = f as Function of (),() ;
hereby :: thesis: ( ( for p being Point of ()
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) ) implies f is continuous )
assume A2: f is continuous ; :: thesis: for p being Point of ()
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r)

let p be Point of (); :: thesis: for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r)
let r be positive Real; :: thesis: ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r)
reconsider p1 = p as Point of () by EUCLID:67;
reconsider q1 = f . p as Point of () by EUCLID:67;
f1 is continuous by ;
then consider s being positive Real such that
A3: f1 .: (Ball (p1,s)) c= Ball (q1,r) by Th17;
take s = s; :: thesis: f .: (Ball (p,s)) c= Ball ((f . p),r)
( Ball (p1,s) = Ball (p,s) & Ball (q1,r) = Ball ((f . p),r) ) by TOPREAL9:13;
hence f .: (Ball (p,s)) c= Ball ((f . p),r) by A3; :: thesis: verum
end;
assume A4: for p being Point of ()
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) ; :: thesis: f is continuous
for p being Point of ()
for q being Point of ()
for r being positive Real st q = f1 . p holds
ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)
proof
let p be Point of (); :: thesis: for q being Point of ()
for r being positive Real st q = f1 . p holds
ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

let q be Point of (); :: thesis: for r being positive Real st q = f1 . p holds
ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

let r be positive Real; :: thesis: ( q = f1 . p implies ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r) )
assume A5: q = f1 . p ; :: thesis: ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)
reconsider p1 = p as Point of () by EUCLID:67;
consider s being positive Real such that
A6: f .: (Ball (p1,s)) c= Ball ((f . p1),r) by A4;
take s ; :: thesis: f1 .: (Ball (p,s)) c= Ball (q,r)
( Ball (p1,s) = Ball (p,s) & Ball ((f . p1),r) = Ball (q,r) ) by ;
hence f1 .: (Ball (p,s)) c= Ball (q,r) by A6; :: thesis: verum
end;
then f1 is continuous by Th17;
hence f is continuous by ; :: thesis: verum