theorem Th32: :: LOPBAN10:45

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
for g being Lipschitzian MultilinearOperator of X,Y st g = f holds
for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t)