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

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