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