let X, Y, Z be RealNormSpace; :: thesis: for f being Lipschitzian BilinearOperator of X,Y,Z holds (BoundedBilinearOperatorsNorm (X,Y,Z)) . f = upper_bound (PreNorms f)
let f be Lipschitzian BilinearOperator of X,Y,Z; :: thesis: (BoundedBilinearOperatorsNorm (X,Y,Z)) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
f in BoundedBilinearOperators (X,Y,Z) by Def9;
hence (BoundedBilinearOperatorsNorm (X,Y,Z)) . f = upper_bound (PreNorms (modetrans (f9,X,Y,Z))) by Def13
.= upper_bound (PreNorms f) ;
:: thesis: verum