let V be non empty right_complementable add-associative right_zeroed translatible RLSMetrStruct ; :: thesis: for v, w being Element of holds dist v,w = Norm (w - v)
let v, w be Element of ; :: 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