for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexLinearSpace ;