set C = C_Normed_Algebra_of_ContinuousFunctions X;
A1: ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Th27a;
A2: for x, y being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for a being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ) & ( x = 0. (C_Normed_Algebra_of_ContinuousFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th27a, Th27b, Th27c, Th27d;
thus ( C_Normed_Algebra_of_ContinuousFunctions X is discerning & C_Normed_Algebra_of_ContinuousFunctions X is reflexive & C_Normed_Algebra_of_ContinuousFunctions X is ComplexNormSpace-like ) by NORMSP_0:def 5, NORMSP_0:def 6, CLVECT_1:def 13, A1, A2; :: thesis: verum