for X being non empty set
for Y being ComplexNormSpace
for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)