theorem :: LOPBAN10:29

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is Subspace of R_VectorSpace_of_MultilinearOperators (X,Y) by RSSPACE:11;