let a, b be Real; :: thesis: for RNS being RealNormSpace
for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + (|.b.| * ||.y.||)
let RNS be RealNormSpace; :: thesis: for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + (|.b.| * ||.y.||)
let x, y be Point of RNS; :: thesis: ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + (|.b.| * ||.y.||)
||.((a * x) + (b * y)).|| <= ||.(a * x).|| + ||.(b * y).|| by Def1;
then ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + ||.(b * y).|| by Def1;
hence ||.((a * x) + (b * y)).|| <= (|.a.| * ||.x.||) + (|.b.| * ||.y.||) by Def1; :: thesis: verum