:: deftheorem defines R_VectorSpace_of_LinearOperators LOPBAN_1:def 7 :
for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators (X,Y) = RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);