let X be non empty compact TopSpace; :: thesis: for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(F + G).|| <= ||.F.|| + ||.G.||
let F, G be Point of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ||.(F + G).|| <= ||.F.|| + ||.G.||
reconsider F1 = F, G1 = G as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A1: ||.F.|| = ||.F1.|| by FUNCT_1:49;
A2: ||.G.|| = ||.G1.|| by FUNCT_1:49;
A3: ||.(F + G).|| = ||.(F1 + G1).|| by Lm4, Lm3;
thus ||.(F + G).|| <= ||.F.|| + ||.G.|| by A1, A2, A3, CC0SP1:25; :: thesis: verum