theorem Th25: :: CSSPACE:30

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