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