:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def 2 :
for IT being non empty UNITSTR holds
( IT is RealUnitarySpace-like iff for x, y, z being Point of IT
for a being Real holds
( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) );