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