for z1, z2 being Complex
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)