theorem :: CC0SP2:19

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