take f = id the carrier of V; :: thesis: ( f is onto & f is isometric )

thus rng f = the carrier of V ; :: 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))

thus dist (x,y) = dist ((f . x),y)

.= dist ((f . x),(f . y)) ; :: thesis: verum

thus rng f = the carrier of V ; :: 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))

thus dist (x,y) = dist ((f . x),y)

.= dist ((f . x),(f . y)) ; :: thesis: verum