theorem
for
X being non
empty set for
Y being
RealNormSpace holds
RLSStruct(#
(BoundedFunctions (X,Y)),
(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is
Subspace of
RealVectSpace (
X,
Y)
by Th6, RSSPACE:11;