let X be RealNormSpace-Sequence; for Y being RealNormSpace holds R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace
let Y be RealNormSpace; R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace
RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is RealLinearSpace
;
hence
R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace
by Th38, RSSPACE3:2; verum