theorem :: CSSPACE:16

for X being ComplexUnitarySpace holds (0. X) .|. (0. X) = 0 by Def11;