theorem Th24: :: CSSPACE:29

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