theorem ZERXI: :: LOPBAN11:5

for X being RealNormSpace-Sequence
for z being Element of (product X) st z = 0. (product X) holds
for i being Element of dom X holds z . i = 0. (X . i)