A1: rng f = [#] V by FUNCT_2:def 3;
hence rng (f ") = the carrier of V by TOPS_2:49; :: according to FUNCT_2:def 3 :: thesis: f " is isometric
let x, y be Element of V; :: according to VECTMETR:def 3 :: thesis: 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; :: thesis: verum