theorem Th25: :: LOPBAN14:24

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