let X be non empty set ; :: thesis: for Y being ComplexNormSpace
for f being bounded Function of X,the carrier of Y holds (ComplexBoundedFunctionsNorm X,Y) . f = sup (PreNorms f)
let Y be ComplexNormSpace; :: thesis: for f being bounded Function of X,the carrier of Y holds (ComplexBoundedFunctionsNorm X,Y) . f = sup (PreNorms f)
let f be bounded Function of X,the carrier of Y; :: thesis: (ComplexBoundedFunctionsNorm X,Y) . f = sup (PreNorms f)
A1: f in ComplexBoundedFunctions X,Y by Def5;
reconsider f' = f as set ;
thus (ComplexBoundedFunctionsNorm X,Y) . f = sup (PreNorms (modetrans f',X,Y)) by A1, Def9
.= sup (PreNorms f) by Th17 ; :: thesis: verum