theorem LM01: :: LOPBAN11:12

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being MultilinearOperator of X,Y
for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds
for v0 being Point of (product X) ex M being Real st
( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds
ex F being FinSequence of REAL st
( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )