theorem Th33: :: NDIFF_5:33

for G being RealNormSpace-Sequence
for i, j being Element of dom G
for x being Point of (G . i)
for z being Element of product (carr G) st z = (reproj (i,(0. (product G)))) . x holds
( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )