let X be non empty TopSpace; :: thesis: C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like
for x, y being Point of (C_Normed_Space_of_C_0_Functions X)
for a being Complex holds
( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th45;
hence C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like by CLVECT_1:def 13; :: thesis: verum