:: deftheorem defines R_VectorSpace_of_BilinearOperators LOPBAN_9:def 2 :
for X, Y, Z being RealLinearSpace holds R_VectorSpace_of_BilinearOperators (X,Y,Z) = RLSStruct(# (BilinearOperators (X,Y,Z)),(Zero_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Add_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Mult_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))) #);