for X being RealNormSpace-Sequence
for Y being RealNormSpace holds R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace