:: deftheorem Def3 defines isometric VECTMETR:def 3 :
for V being non empty MetrStruct
for f being Function of V,V holds
( f is isometric iff for x, y being Element of V holds dist (x,y) = dist ((f . x),(f . y)) );