set R = R_Normed_Algebra_of_ContinuousFunctions X;
thus ||.(0. (R_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Th18; :: according to NORMSP_0:def 6 :: thesis: ( R_Normed_Algebra_of_ContinuousFunctions X is discerning & R_Normed_Algebra_of_ContinuousFunctions X is RealNormSpace-like )
for x, y being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( x = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th18;
hence ( R_Normed_Algebra_of_ContinuousFunctions X is discerning & R_Normed_Algebra_of_ContinuousFunctions X is RealNormSpace-like ) by NORMSP_1:def 1; :: thesis: verum