:: deftheorem Def13 defines ComplexNormSpace-like CLVECT_1:def 13 :
for IT being non empty CNORMSTR holds
( IT is ComplexNormSpace-like iff for x, y being Point of IT
for z being Complex holds
( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );