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