:: deftheorem Def14 defines BoundedLinearFunctionalsNorm DUALSP04:def 11 :
for X being RealUnitarySpace
for b₂ being Function of (BoundedLinearFunctionals X),REAL holds
( b₂ = BoundedLinearFunctionalsNorm X iff for x being object st x in BoundedLinearFunctionals X holds
b₂ . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) );