:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CC0SP1:def 9 :
for X being non empty set
for b₂ being Function of (ComplexBoundedFunctions X),REAL holds
( b₂ = ComplexBoundedFunctionsNorm X iff for x being object st x in ComplexBoundedFunctions X holds
b₂ . x = upper_bound (PreNorms (modetrans (x,X))) );