let X be non empty TopSpace; :: thesis: R_Normed_Space_of_C_0_Functions X is RealNormSpace-like
for x, y being Point of (R_Normed_Space_of_C_0_Functions X)
for a being Real holds
( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th34;
hence R_Normed_Space_of_C_0_Functions X is RealNormSpace-like by NORMSP_1:def 1; :: thesis: verum