:: deftheorem Def1 defines isometric MAZURULM:def 1 :
for E, F being non empty NORMSTR
for f being Function of E,F holds
( f is isometric iff for a, b being Point of E holds ||.((f . a) - (f . b)).|| = ||.(a - b).|| );