theorem Th17: :: TOPS_4:17

for M1, M2 being non empty MetrSpace
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) )