:: deftheorem defines R_NormSpace_of_BoundedMultilinearOperators LOPBAN10:def 16 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds R_NormSpace_of_BoundedMultilinearOperators (X,Y) = NORMSTR(# (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)))),(BoundedMultilinearOperatorsNorm (X,Y)) #);