let V be non empty MetrStruct ; :: thesis: id V is isometric
thus rng (id V) = the carrier of V by RELAT_1:71; :: according to VECTMETR:def 3 :: thesis: for x, y being Element of V holds dist x,y = dist ((id V) . x),((id V) . y)
let x, y be Element of V; :: 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