let X be ComplexUnitarySpace; :: thesis: for x being Point of X holds dist (x,x) = 0
let x be Point of X; :: thesis: dist (x,x) = 0
thus dist (x,x) = ||.H₁(X).|| by RLVECT_1:15
.= 0 by Th37 ; :: thesis: verum