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