let a be Real; :: thesis: for X being non empty compact TopSpace
for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let X be non empty compact TopSpace; :: thesis: for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
reconsider F1 = F, G1 = G as Point of (R_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;
( ||.F1.|| = 0 iff F1 = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by C0SP1:32;
hence ( ||.F.|| = 0 iff F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) by Lm7, FUNCT_1:49; :: thesis: ( ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
thus ||.(a * F).|| = ||.(a * F1).|| by Lm5, Lm3
.= |.a.| * ||.F1.|| by C0SP1:32
.= |.a.| * ||.F.|| by FUNCT_1:49 ; :: thesis: ||.(F + G).|| <= ||.F.|| + ||.G.||
thus ||.(F + G).|| <= ||.F.|| + ||.G.|| by A1, A2, A3, C0SP1:32; :: thesis: verum