theorem Th30: :: LOPBAN10:43

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Lipschitzian MultilinearOperator of X,Y holds (BoundedMultilinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)