let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace holds the carrier of S --> (0. T) = 0. (R_NormSpace_of_ContinuousFunctions (S,T))
let T be NormedLinearTopSpace; :: thesis: the carrier of S --> (0. T) = 0. (R_NormSpace_of_ContinuousFunctions (S,T))
the carrier of S --> (0. T) = 0. (R_VectorSpace_of_ContinuousFunctions (S,T)) by Th9;
hence the carrier of S --> (0. T) = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) ; :: thesis: verum