let X, Y be ComplexNormSpace; :: thesis: for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)

let f be Lipschitzian LinearOperator of X,Y; :: thesis: (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)

reconsider f9 = f as set ;

f in BoundedLinearOperators (X,Y) by Def7;

hence (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def11

.= upper_bound (PreNorms f) by Th28 ;

:: thesis: verum

let f be Lipschitzian LinearOperator of X,Y; :: thesis: (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)

reconsider f9 = f as set ;

f in BoundedLinearOperators (X,Y) by Def7;

hence (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def11

.= upper_bound (PreNorms f) by Th28 ;

:: thesis: verum