:: deftheorem defines ||. BHSP_1:def 4 :
for X being RealUnitarySpace
for x being Point of X holds ||.x.|| = sqrt (x .|. x);