let X, Y be RealNormSpace; :: thesis: for f being bounded LinearOperator of X,Y holds (BoundedLinearOperatorsNorm X,Y) . f = upper_bound (PreNorms f)
let f be bounded LinearOperator of X,Y; :: thesis: (BoundedLinearOperatorsNorm X,Y) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
f in BoundedLinearOperators X,Y by Def10;
hence (BoundedLinearOperatorsNorm X,Y) . f = upper_bound (PreNorms (modetrans f9,X,Y)) by Def14
.= upper_bound (PreNorms f) by Th35 ;
:: thesis: verum