theorem Th49: :: NDIFF_5:49

for G being RealNormSpace-Sequence
for i, j being Element of dom G
for x, y being Point of (product G)
for xi being Point of (G . i) st y = (reproj (i,x)) . xi & i <> j holds
(proj j) . x = (proj j) . y