let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace holds 0. (R_Normed_Space_of_C_0_Functions (X,T)) = X --> (0. T)
let T be NormedLinearTopSpace; :: thesis: 0. (R_Normed_Space_of_C_0_Functions (X,T)) = X --> (0. T)
0. (R_Normed_Space_of_C_0_Functions (X,T)) = 0. (R_VectorSpace_of_C_0_Functions (X,T))
.= X --> (0. T) by Th62 ;
hence 0. (R_Normed_Space_of_C_0_Functions (X,T)) = X --> (0. T) ; :: thesis: verum