:: deftheorem defines ||. CSSPACE:def 15 :
for X being ComplexUnitarySpace
for x being Point of X holds ||.x.|| = sqrt |.(x .|. x).|;