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