A1:
rng f = [#] V
by FUNCT_2:def 3;
hence
rng (f ") = the carrier of V
by TOPS_2:49; FUNCT_2:def 3 f " is isometric
let x, y be Element of V; VECTMETR:def 3 dist (x,y) = dist (((f ") . x),((f ") . y))
A2:
rng f = the carrier of V
by A1;
then A3:
dom (f ") = [#] V
by TOPS_2:49;
A4: y =
(id (rng f)) . y
by A2
.=
(f * (f ")) . y
by A1, TOPS_2:52
.=
f . ((f ") . y)
by A3, FUNCT_1:13
;
x =
(id (rng f)) . x
by A2
.=
(f * (f ")) . x
by A1, TOPS_2:52
.=
f . ((f ") . x)
by A3, FUNCT_1:13
;
hence
dist (x,y) = dist (((f ") . x),((f ") . y))
by A4, Def3; verum