theorem
for
X,
Y being
RealNormSpace holds
RLSStruct(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is
Subspace of
R_VectorSpace_of_LinearOperators (
X,
Y)
by Th22, RSSPACE:11;