A1: C_VectorSpace_of_C_0_Functions X is ComplexLinearSpace ;
A2: for x being Point of (C_Normed_Space_of_C_0_Functions X) st ||.x.|| = 0 holds
x = 0. (C_Normed_Space_of_C_0_Functions X) by Th46;
||.(0. (C_Normed_Space_of_C_0_Functions X)).|| = 0 by Th46;
hence ( C_Normed_Space_of_C_0_Functions X is reflexive & C_Normed_Space_of_C_0_Functions X is discerning & C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like & C_Normed_Space_of_C_0_Functions X is vector-distributive & C_Normed_Space_of_C_0_Functions X is scalar-distributive & C_Normed_Space_of_C_0_Functions X is scalar-associative & C_Normed_Space_of_C_0_Functions X is scalar-unital & C_Normed_Space_of_C_0_Functions X is Abelian & C_Normed_Space_of_C_0_Functions X is add-associative & C_Normed_Space_of_C_0_Functions X is right_zeroed & C_Normed_Space_of_C_0_Functions X is right_complementable ) by A1, A2, Lm15, CSSPACE3:2; :: thesis: verum