theorem :: LOPBAN10:25

for G being RealNormSpace-Sequence
for p being Point of (product G) holds
( 0. (product G) = p iff for i being Element of dom G holds p . i = 0. (G . i) )