A1: rng f = [#] V by FUNCT_2:def 3;
hence rng (f ") = the carrier of V by TOPS_2:62; :: 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:62;
A4: y = (id (rng f)) . y by A2, FUNCT_1:35
.= (f * (f ")) . y by A1, TOPS_2:65
.= f . ((f ") . y) by A3, FUNCT_1:23 ;
x = (id (rng f)) . x by A2, FUNCT_1:35
.= (f * (f ")) . x by A1, TOPS_2:65
.= f . ((f ") . x) by A3, FUNCT_1:23 ;
hence dist (x,y) = dist (((f ") . x),((f ") . y)) by A4, Def3; :: thesis: verum