let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace
for f being Lipschitzian MultilinearOperator of X,Y holds (BoundedMultilinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
let Y be RealNormSpace; :: thesis: for f being Lipschitzian MultilinearOperator of X,Y holds (BoundedMultilinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
let f be Lipschitzian MultilinearOperator of X,Y; :: thesis: (BoundedMultilinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
f in BoundedMultilinearOperators (X,Y) by Def9;
hence (BoundedMultilinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def13
.= upper_bound (PreNorms f) ;
:: thesis: verum