:: deftheorem Def13 defines BoundedMultilinearOperatorsNorm LOPBAN10:def 15 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for b₃ being Function of (BoundedMultilinearOperators (X,Y)),REAL holds
( b₃ = BoundedMultilinearOperatorsNorm (X,Y) iff for x being object st x in BoundedMultilinearOperators (X,Y) holds
b₃ . x = upper_bound (PreNorms (modetrans (x,X,Y))) );