for S being non empty compact TopSpace
for T being NormedLinearTopSpace st T is complete holds
R_NormSpace_of_ContinuousFunctions (S,T) is complete