let X be ComplexUnitarySpace; :: thesis: for x, y, z being Point of X holds dist ((x - z),(y - z)) = dist (x,y)
let x, y, z 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:29
.= ||.((x - (y + z)) + z).|| by RLVECT_1:27
.= ||.(((x - y) - z) + z).|| by RLVECT_1:27
.= ||.((x - y) - (z - z)).|| by RLVECT_1:29
.= ||.((x - y) - H₁(X)).|| by RLVECT_1:15
.= dist (x,y) by RLVECT_1:13 ; :: thesis: verum