theorem Th12: :: MAZURULM:12

for E, F being RealNormSpace
for f being Function of E,F st f is bijective & f is isometric holds
f /" is isometric