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 = upper_bound (PreNorms f)

let Y be ComplexNormSpace; :: thesis: for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)

let f be bounded Function of X, the carrier of Y; :: thesis: (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)

reconsider f9 = f as set ;

f in ComplexBoundedFunctions (X,Y) by Def5;

hence (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def9

.= upper_bound (PreNorms f) by Th14 ;

:: thesis: verum

for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)

let Y be ComplexNormSpace; :: thesis: for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)

let f be bounded Function of X, the carrier of Y; :: thesis: (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)

reconsider f9 = f as set ;

f in ComplexBoundedFunctions (X,Y) by Def5;

hence (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def9

.= upper_bound (PreNorms f) by Th14 ;

:: thesis: verum