for S being non empty MetrSpace
for V being non empty compact TopSpace
for T being NormedLinearTopSpace
for f being Function of V,T st V = TopSpaceMetr S holds
( f is continuous iff for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < e ) ) )