:: deftheorem Def17 defines BoundedFunctionsNorm C0SP1:def 17 :
for X being non empty set
for b₂ being Function of (BoundedFunctions X),REAL holds
( b₂ = BoundedFunctionsNorm X iff for x being object st x in BoundedFunctions X holds
b₂ . x = upper_bound (PreNorms (modetrans (x,X))) );