theorem LM35: :: LOPBAN10:39

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for g being MultilinearOperator of X,Y
for a being FinSequence of REAL st dom a = dom X holds
for t, t1 being Point of (product X) st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = (Product a) * (g . t)