( f * g is onto & f * g is isometric )
_{1} being Function of V,V st b_{1} = f * g holds

( b_{1} is onto & b_{1} is isometric )
; :: thesis: verum

proof

hence
for b
rng g =
the carrier of V
by FUNCT_2:def 3

.= dom f by FUNCT_2:def 1 ;

hence rng (f * g) = rng f by RELAT_1:28

.= the carrier of V by FUNCT_2:def 3 ;

:: according to FUNCT_2:def 3 :: thesis: f * g is isometric

let x, y be Element of V; :: according to VECTMETR:def 3 :: thesis: dist (x,y) = dist (((f * g) . x),((f * g) . y))

x in the carrier of V ;

then A1: x in dom g by FUNCT_2:def 1;

y in the carrier of V ;

then A2: 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:13

.= dist (((f * g) . x),((f * g) . y)) by A2, FUNCT_1:13 ; :: thesis: verum

end;.= dom f by FUNCT_2:def 1 ;

hence rng (f * g) = rng f by RELAT_1:28

.= the carrier of V by FUNCT_2:def 3 ;

:: according to FUNCT_2:def 3 :: thesis: f * g is isometric

let x, y be Element of V; :: according to VECTMETR:def 3 :: thesis: dist (x,y) = dist (((f * g) . x),((f * g) . y))

x in the carrier of V ;

then A1: x in dom g by FUNCT_2:def 1;

y in the carrier of V ;

then A2: 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:13

.= dist (((f * g) . x),((f * g) . y)) by A2, FUNCT_1:13 ; :: thesis: verum

( b