theorem Th20: :: C0SP1:20

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