theorem :: TOPS_4:15

for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is continuous iff for p being Point of T
for q being Point of M
for r being positive Real st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )