theorem :: LOPBAN10:27

for X being RealNormSpace-Sequence
for x being Point of (product X) holds
( ( ex i being Element of dom X st x . i = 0. (X . i) implies NrProduct x = 0 ) & ( NrProduct x = 0 implies ex i being Element of dom X st x . i = 0. (X . i) ) & ( ( for i being Element of dom X holds not x . i = 0. (X . i) ) implies 0 < NrProduct x ) )