thus rng (id V) = the carrier of V by RELAT_1:71; :: according to FUNCT_2:def 3 :: thesis: id V is isometric
let x, y be Element of V; :: according to VECTMETR:def 3 :: thesis: dist (x,y) = dist (((id V) . x),((id V) . y))
thus dist (x,y) = dist (((id V) . x),y) by FUNCT_1:35
.= dist (((id V) . x),((id V) . y)) by FUNCT_1:35 ; :: thesis: verum