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