theorem :: CC0SP2:47

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