theorem Th6: :: CSSPACE3:7

for x, y being Point of Complex_l1_Space
for p being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )