let X be non empty set ; :: thesis: ( C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )
thus ||.(0. (C_Normed_Algebra_of_BoundedFunctions X)).|| = 0 by Th29; :: according to NORMSP_0:def 6 :: thesis: ( C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )
for x, y being Point of (C_Normed_Algebra_of_BoundedFunctions X)
for a being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( x = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th29;
hence ( C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like ) by CLVECT_1:def 13, NORMSP_0:def 5; :: thesis: verum