let X be non empty set ; :: thesis: for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
let Y be RealNormSpace; :: thesis: for f being bounded Function of X, the carrier of Y holds (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
let f be bounded Function of X, the carrier of Y; :: thesis: (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
f in BoundedFunctions (X,Y) by Def5;
hence (BoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def9
.= upper_bound (PreNorms f) by Th13 ;
:: thesis: verum