:: deftheorem Def13 defines BoundedLinearOperatorsNorm LOPBAN_1:def 13 :
for X, Y being RealNormSpace
for b₃ being Function of (BoundedLinearOperators (X,Y)),REAL holds
( b₃ = BoundedLinearOperatorsNorm (X,Y) iff for x being object st x in BoundedLinearOperators (X,Y) holds
b₃ . x = upper_bound (PreNorms (modetrans (x,X,Y))) );