let X be ComplexUnitarySpace; :: thesis: for x, z, y being Point of X holds dist (x - z),(y - z) = dist x,y
let x, z, y be Point of X; :: thesis: dist (x - z),(y - z) = dist x,y
thus dist (x - z),(y - z) = ||.(((x - z) - y) + z).|| by RLVECT_1:43
.= ||.((x - (y + z)) + z).|| by RLVECT_1:41
.= ||.(((x - y) - z) + z).|| by RLVECT_1:41
.= ||.((x - y) - (z - z)).|| by RLVECT_1:43
.= ||.((x - y) - H₁(X)).|| by RLVECT_1:28
.= dist x,y by RLVECT_1:26 ; :: thesis: verum