:: deftheorem Def11 defines ComplexUnitarySpace-like CSSPACE:def 13 :
for IT being non empty CUNITSTR holds
( IT is ComplexUnitarySpace-like iff for x, y, w being Point of IT
for a being Complex holds
( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. w = (x .|. w) + (y .|. w) & (a * x) .|. y = a * (x .|. y) ) );