let X be non empty TopSpace; :: thesis: 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0
A1: C_VectorSpace_of_C_0_Functions X is Subspace of ComplexVectSpace the carrier of X by Th41;
0. (ComplexVectSpace the carrier of X) = X --> 0 ;
hence 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0 by A1, CLVECT_1:30; :: thesis: verum