theorem :: LOPBAN10:10

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is Subspace of RealVectSpace ( the carrier of (product X),Y) by RSSPACE:11;