theorem LM32: :: LOPBAN10:36

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for g being MultilinearOperator of X,Y
for t being Point of (product X) st ex i being Element of dom X st t . i = 0. (X . i) holds
g . t = 0. Y