let a be Real; :: thesis: for X being non empty TopSpace
for T being NormedLinearTopSpace
for F, G being Point of (R_Normed_Space_of_C_0_Functions (X,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for F, G being Point of (R_Normed_Space_of_C_0_Functions (X,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let T be NormedLinearTopSpace; :: thesis: for F, G being Point of (R_Normed_Space_of_C_0_Functions (X,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) 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,T)); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) 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,T)) )
proof
reconsider FB = F as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) by Th60;
A2: 0. (R_Normed_Space_of_C_0_Functions (X,T)) = X --> (0. T) by Th63;
( ||.FB.|| = 0 iff FB = 0. (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) ) by RSSPACE4:21;
hence ( ||.F.|| = 0 iff F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) ) by A2, RSSPACE4:15, FUNCT_1:49; :: thesis: verum
end;
A3: ||.(a * F).|| = |.a.| * ||.F.||
proof
reconsider FB = F as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) by Th60;
A4: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A5: a * FB = a * F by Th65;
reconsider aFB = a * FB as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) ;
reconsider aF = a * F as Point of (R_Normed_Space_of_C_0_Functions (X,T)) ;
||.aFB.|| = ||.aF.|| by A5, FUNCT_1:49;
hence ||.(a * F).|| = |.a.| * ||.F.|| by A4, RSSPACE4:21; :: thesis: verum
end;
||.(F + G).|| <= ||.F.|| + ||.G.||
proof
reconsider FB = F, GB = G as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) by Th60;
A6: ( ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| ) by FUNCT_1:49;
FB + GB = F + G by Th64;
then ||.(FB + GB).|| = ||.(F + G).|| by FUNCT_1:49;
hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A6, RSSPACE4:21; :: thesis: verum
end;
hence ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions (X,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A3; :: thesis: verum