:: deftheorem Def2 defines isometric JORDAN24:def 2 :
for M being non empty MetrStruct
for f being Function of (TopSpaceMetr M),(TopSpaceMetr M) holds
( f is isometric iff ex g being isometric Function of M,M st g = f );