for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace ;