theorem Th40: :: C0SP3:40

for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds the carrier of S --> (0. T) = 0. (R_NormSpace_of_ContinuousFunctions (S,T))