:: deftheorem Def13 defines BoundedBilinearOperatorsNorm LOPBAN_9:def 8 :
for X, Y, Z being RealNormSpace
for b₄ being Function of (BoundedBilinearOperators (X,Y,Z)),REAL holds
( b₄ = BoundedBilinearOperatorsNorm (X,Y,Z) iff for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b₄ . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) );