let X be non empty set ; :: thesis: for f being Function of X,COMPLEX st f | X is bounded holds

(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

let f be Function of X,COMPLEX; :: thesis: ( f | X is bounded implies (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f) )

assume A1: f | X is bounded ; :: thesis: (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

then f in ComplexBoundedFunctions X ;

then (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms (modetrans (f,X))) by Def9;

hence (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f) by Th12, A1; :: thesis: verum

(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

let f be Function of X,COMPLEX; :: thesis: ( f | X is bounded implies (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f) )

assume A1: f | X is bounded ; :: thesis: (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

then f in ComplexBoundedFunctions X ;

then (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms (modetrans (f,X))) by Def9;

hence (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f) by Th12, A1; :: thesis: verum