for X, Y, Z being RealLinearSpace holds 0. (R_VectorSpace_of_BilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z)