theorem :: LOPBAN_9:1

for X, Y, Z being RealLinearSpace holds R_VectorSpace_of_BilinearOperators (X,Y,Z) is Subspace of RealVectSpace ( the carrier of [:X,Y:],Z) by RSSPACE:11;