for X being ComplexUnitarySpace
for x being Point of X holds x, 0. X are_orthogonal