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).|| = |.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).|| = |.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).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
A1: ( ||.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;
A2: 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 A2, C0SP1:25, FUNCT_1:49; :: thesis: verum
end;
A3: ||.(a * F).|| = |.a.| * ||.F.||
proof
reconsider FB = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;
A4: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A5: a * FB = a * F by Lm14;
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 A5, FUNCT_1:49;
hence ||.(a * F).|| = |.a.| * ||.F.|| by A4, 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;
A6: ( ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| ) by FUNCT_1:49;
FB + GB = F + G by Lm13;
then A7: ||.(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 A7, A6, 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).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A3; :: thesis: verum