let X be 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)
let Y be RealNormSpace; 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; (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
;
verum