let X be non empty set ; :: thesis: for f being Function of X,REAL st f | X is bounded holds
(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
let f be Function of X,REAL; :: thesis: ( f | X is bounded implies (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f) )
reconsider f9 = f as set ;
assume A1: f | X is bounded ; :: thesis: (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
then f in BoundedFunctions X ;
then (BoundedFunctionsNorm X) . f = upper_bound (PreNorms (modetrans (f9,X))) by Def17;
hence (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f) by A1, Th19; :: thesis: verum