A1: R_VectorSpace_of_C_0_Functions X is RealLinearSpace ;
A2: for x being Point of (R_Normed_Space_of_C_0_Functions X) st ||.x.|| = 0 holds
x = 0. (R_Normed_Space_of_C_0_Functions X) by Th34;
||.(0. (R_Normed_Space_of_C_0_Functions X)).|| = 0 by Th34;
hence ( R_Normed_Space_of_C_0_Functions X is reflexive & R_Normed_Space_of_C_0_Functions X is discerning & R_Normed_Space_of_C_0_Functions X is RealNormSpace-like & R_Normed_Space_of_C_0_Functions X is vector-distributive & R_Normed_Space_of_C_0_Functions X is scalar-distributive & R_Normed_Space_of_C_0_Functions X is scalar-associative & R_Normed_Space_of_C_0_Functions X is scalar-unital & R_Normed_Space_of_C_0_Functions X is Abelian & R_Normed_Space_of_C_0_Functions X is add-associative & R_Normed_Space_of_C_0_Functions X is right_zeroed & R_Normed_Space_of_C_0_Functions X is right_complementable ) by A1, A2, Th35, RSSPACE3:2; :: thesis: verum