for a, b being Real
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + (|.b.| * ||.y.||)