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