theorem Th38: :: NDIFF_5:38

for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of (G . i) st x <> 0. (G . i) holds
(reproj (i,(0. (product G)))) . x <> 0. (product G)