let E, F be RealNormSpace; :: thesis: for f being Function of E,F st f is bijective & f is isometric holds
f /" is isometric
let f be Function of E,F; :: thesis: ( f is bijective & f is isometric implies f /" is isometric )
assume that
A1: f is bijective and
A2: f is isometric ; :: thesis: f /" is isometric
set g = f /" ;
let a, b be Point of F; :: according to MAZURULM:def 1 :: thesis: ||.(((f /") . a) - ((f /") . b)).|| = ||.(a - b).||
( f . ((f /") . a) = a & f . ((f /") . b) = b ) by A1, Lm2;
hence ||.(((f /") . a) - ((f /") . b)).|| = ||.(a - b).|| by A2; :: thesis: verum