take f = id the carrier of V; :: thesis: ( f is onto & f is isometric )
thus rng f = the carrier of V by RELAT_1:71; :: 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 by FUNCT_1:35
.= dist (f . x),(f . y) by FUNCT_1:35 ; :: thesis: verum