theorem :: LOPBAN10:8

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