let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace holds 0. (R_NormSpace_of_ContinuousFunctions (S,T)) = 0. (R_NormSpace_of_BoundedFunctions ( the carrier of S,T))
let T be NormedLinearTopSpace; :: thesis: 0. (R_NormSpace_of_ContinuousFunctions (S,T)) = 0. (R_NormSpace_of_BoundedFunctions ( the carrier of S,T))
thus 0. (R_NormSpace_of_ContinuousFunctions (S,T)) = the carrier of S --> (0. T) by Th40
.= 0. (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by RSSPACE4:15 ; :: thesis: verum