let X be non empty set ; :: thesis: for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
let Y be RealNormSpace; :: thesis: 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
( R_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of RealVectSpace (X,Y) & 0. (RealVectSpace (X,Y)) = X --> (0. Y) ) by Th7, LOPBAN_1:16, RSSPACE:13;
hence 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) by RLSUB_1:19; :: thesis: verum