theorem LM02: :: LOPBAN11:11

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, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||