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:28
.= 0 by Th44 ; :: thesis: verum