theorem Th30: :: LOPBAN_1:30

for X, Y being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)