( 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
;
FUNCT_2:def 3 f * g is isometric
let x,
y be
Element of
V;
VECTMETR:def 3 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
;
verum
end;
hence
for b1 being Function of V,V st b1 = f * g holds
( b1 is onto & b1 is isometric )
; verum