:: deftheorem defines R_VectorSpace_of_MultilinearOperators LOPBAN10:def 5 :
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds R_VectorSpace_of_MultilinearOperators (X,Y) = 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)))) #);