let X be non empty TopSpace; :: thesis: 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0
0. (C_Normed_Space_of_C_0_Functions X) = 0. (C_VectorSpace_of_C_0_Functions X)
.= X --> 0 by Th44 ;
hence 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 ; :: thesis: verum