theorem :: LOPBAN14:10

for X, Y being RealLinearSpace holds R_VectorSpace_of_MultilinearOperators (<*X*>,Y) = R_VectorSpace_of_LinearOperators ((product <*X*>),Y)