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:16 ; :: thesis: verum