let V be non empty right_complementable add-associative right_zeroed translatible RLSMetrStruct ; :: thesis: for v, w being Element of V holds dist (v,w) = Norm (w - v)
let v, w be Element of V; :: thesis: dist (v,w) = Norm (w - v)
thus dist (v,w) = dist ((v + (- v)),(w + (- v))) by Def6
.= Norm (w - v) by RLVECT_1:5 ; :: thesis: verum