let M be non empty MetrSpace; :: thesis: for x being Point of M holds (dist x) . x = 0
let x be Point of M; :: thesis: (dist x) . x = 0
(dist x) . x = dist (x,x) by WEIERSTR:def 4
.= 0 by METRIC_1:1 ;
hence (dist x) . x = 0 ; :: thesis: verum