let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace holds 0. (R_VectorSpace_of_C_0_Functions (X,T)) = X --> (0. T)
let T be NormedLinearTopSpace; :: thesis: 0. (R_VectorSpace_of_C_0_Functions (X,T)) = X --> (0. T)
A1: R_VectorSpace_of_C_0_Functions (X,T) is Subspace of RealVectSpace ( the carrier of X,T) by RSSPACE:11;
0. (RealVectSpace ( the carrier of X,T)) = X --> (0. T) ;
hence 0. (R_VectorSpace_of_C_0_Functions (X,T)) = X --> (0. T) by A1, RLSUB_1:11; :: thesis: verum