let V be non empty MetrStruct ; :: thesis: for f, g being isometric Function of V,V holds f * g is isometric
let f, g be isometric Function of V,V; :: thesis: f * g is isometric
rng g = the carrier of V by Def3
.= dom f by FUNCT_2:def 1 ;
hence rng (f * g) = rng f by RELAT_1:47
.= the carrier of V by Def3 ;
:: according to VECTMETR:def 3 :: thesis: for x, y being Element of V holds dist x,y = dist ((f * g) . x),((f * g) . y)
let x, y be Element of V; :: thesis: dist x,y = dist ((f * g) . x),((f * g) . y)
( x in the carrier of V & y in the carrier of V ) ;
then A1: ( x in dom g & y in dom g ) by FUNCT_2:def 1;
thus dist x,y = dist (g . x),(g . y) by Def3
.= dist (f . (g . x)),(f . (g . y)) by Def3
.= dist ((f * g) . x),(f . (g . y)) by A1, FUNCT_1:23
.= dist ((f * g) . x),((f * g) . y) by A1, FUNCT_1:23 ; :: thesis: verum