R_VectorSpace_of_C_0_Functions (X,T) is RealLinearSpace ;
hence ( R_Normed_Space_of_C_0_Functions (X,T) is reflexive & R_Normed_Space_of_C_0_Functions (X,T) is discerning & R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace-like & R_Normed_Space_of_C_0_Functions (X,T) is vector-distributive & R_Normed_Space_of_C_0_Functions (X,T) is scalar-distributive & R_Normed_Space_of_C_0_Functions (X,T) is scalar-associative & R_Normed_Space_of_C_0_Functions (X,T) is scalar-unital & R_Normed_Space_of_C_0_Functions (X,T) is Abelian & R_Normed_Space_of_C_0_Functions (X,T) is add-associative & R_Normed_Space_of_C_0_Functions (X,T) is right_zeroed & R_Normed_Space_of_C_0_Functions (X,T) is right_complementable ) by RSSPACE3:2, Th66; :: thesis: verum