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