theorem Th14: :: NDIFF_5:14

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