let z1, z2 be Complex; :: thesis: for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
let CNS be ComplexNormSpace; :: thesis: for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
let x, y be Point of CNS; :: thesis: ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
||.((z1 * x) + (z2 * y)).|| <= ||.(z1 * x).|| + ||.(z2 * y).|| by Def13;
then ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + ||.(z2 * y).|| by Def13;
hence ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||) by Def13; :: thesis: verum