( f * g is onto & f * g is isometric )

proof

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;

hence for b₁ being Function of V,V st b₁ = f * g holds
( b₁ is onto & b₁ is isometric ) ; :: thesis: verum