theorem Th30: :: LOPBAN_9:14

for X, Y, Z being RealNormSpace
for f being Lipschitzian BilinearOperator of X,Y,Z holds (BoundedBilinearOperatorsNorm (X,Y,Z)) . f = upper_bound (PreNorms f)