for X being ComplexUnitarySpace
for x being Point of X holds (0. X) .|. x = 0