let E, F, G be RealNormSpace; :: thesis: for f being Function of E,F

for g being Function of F,G st f is isometric & g is isometric holds

g * f is isometric

let f be Function of E,F; :: thesis: for g being Function of F,G st f is isometric & g is isometric holds

g * f is isometric

let g be Function of F,G; :: thesis: ( f is isometric & g is isometric implies g * f is isometric )

assume that

A1: f is isometric and

A2: g is isometric ; :: thesis: g * f is isometric

set h = g * f;

let a be Point of E; :: according to MAZURULM:def 1 :: thesis: for b being Point of E holds ||.(((g * f) . a) - ((g * f) . b)).|| = ||.(a - b).||

let b be Point of E; :: thesis: ||.(((g * f) . a) - ((g * f) . b)).|| = ||.(a - b).||

( (g * f) . a = g . (f . a) & (g * f) . b = g . (f . b) ) by FUNCT_2:15;

hence ||.(((g * f) . a) - ((g * f) . b)).|| = ||.((f . a) - (f . b)).|| by A2

.= ||.(a - b).|| by A1 ;

:: thesis: verum

for g being Function of F,G st f is isometric & g is isometric holds

g * f is isometric

let f be Function of E,F; :: thesis: for g being Function of F,G st f is isometric & g is isometric holds

g * f is isometric

let g be Function of F,G; :: thesis: ( f is isometric & g is isometric implies g * f is isometric )

assume that

A1: f is isometric and

A2: g is isometric ; :: thesis: g * f is isometric

set h = g * f;

let a be Point of E; :: according to MAZURULM:def 1 :: thesis: for b being Point of E holds ||.(((g * f) . a) - ((g * f) . b)).|| = ||.(a - b).||

let b be Point of E; :: thesis: ||.(((g * f) . a) - ((g * f) . b)).|| = ||.(a - b).||

( (g * f) . a = g . (f . a) & (g * f) . b = g . (f . b) ) by FUNCT_2:15;

hence ||.(((g * f) . a) - ((g * f) . b)).|| = ||.((f . a) - (f . b)).|| by A2

.= ||.(a - b).|| by A1 ;

:: thesis: verum