for X being RealUnitarySpace
for f being Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)