let X, Y be RealNormSpace; :: thesis: R_NormSpace_of_BoundedMultilinearOperators (<*X*>,Y) = R_NormSpace_of_BoundedLinearOperators ((product <*X*>),Y)
A1: R_VectorSpace_of_MultilinearOperators (<*X*>,Y) = R_VectorSpace_of_LinearOperators ((product <*X*>),Y) by Th25;
BoundedMultilinearOperatorsNorm (<*X*>,Y) = BoundedLinearOperatorsNorm ((product <*X*>),Y) by Th24;
hence R_NormSpace_of_BoundedMultilinearOperators (<*X*>,Y) = R_NormSpace_of_BoundedLinearOperators ((product <*X*>),Y) by A1; :: thesis: verum