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