:: deftheorem Def13 defines BoundedLinearFunctionalsNorm DUALSP01:def 14 :
for X being RealNormSpace
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))) );