let a be Real; :: thesis: for X being non empty TopSpace
for F, G being Point of (R_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let X be non empty TopSpace; :: thesis: for F, G being Point of (R_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_Normed_Space_of_C_0_Functions X); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
L1: ( ||.F.|| = 0 iff F = 0. (R_Normed_Space_of_C_0_Functions X) )

proof

reconsider FB = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;
A4: 0. (R_Normed_Space_of_C_0_Functions X) = X --> 0 by Th33;
( ||.FB.|| = 0 iff FB = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by C0SP1:32;
hence ( ||.F.|| = 0 iff F = 0. (R_Normed_Space_of_C_0_Functions X) ) by A4, C0SP1:25, FUNCT_1:49; :: thesis: verum

end;

L2: ||.(a * F).|| = (abs a) * ||.F.||

proof

reconsider FB = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;
A6: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A7: a * FB = a * F by Lm16;
reconsider aFB = a * FB as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = a * F as Point of (R_Normed_Space_of_C_0_Functions X) ;
||.aFB.|| = ||.aF.|| by A7, FUNCT_1:49;
hence ||.(a * F).|| = (abs a) * ||.F.|| by A6, C0SP1:32; :: thesis: verum

end;

||.(F + G).|| <= ||.F.|| + ||.G.||

proof

reconsider FB = F, GB = G as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;
A10: ( ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| ) by FUNCT_1:49;
FB + GB = F + G by Lm15;
then A11: ||.(FB + GB).|| = ||.(F + G).|| by FUNCT_1:49;
reconsider aFB = FB + GB as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = F, aG = G as Point of (R_Normed_Space_of_C_0_Functions X) ;
thus ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A10, C0SP1:32; :: thesis: verum

end;

hence ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by L1, L2; :: thesis: verum