theorem :: TOPS_4:20
for n, m being Nat
for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) )