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 Th6, LOPBAN_1:13, RSSPACE:11;
hence 0. (R_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) by RLSUB_1:11; :: thesis: verum