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

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