theorem Th29: :: CSSPACE:34

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