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