for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)