theorem :: CSSPACE:45

for X being ComplexUnitarySpace
for x, y being Point of X holds |.(x .|. y).| <= ||.x.|| * ||.y.|| by Th30;