let X, Y be RealLinearSpace; :: thesis: R_VectorSpace_of_MultilinearOperators (<*X*>,Y) = R_VectorSpace_of_LinearOperators ((product <*X*>),Y)
MultilinearOperators (<*X*>,Y) = LinearOperators ((product <*X*>),Y) by Th10;
hence R_VectorSpace_of_MultilinearOperators (<*X*>,Y) = R_VectorSpace_of_LinearOperators ((product <*X*>),Y) ; :: thesis: verum