:: deftheorem defines R_VectorSpace_of_BoundedBilinearOperators LOPBAN_9:def 5 :
for X, Y, Z being RealNormSpace holds R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) = RLSStruct(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))) #);