theorem Th46: :: NDIFF_5:46

for G being RealNormSpace-Sequence
for i 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 holds
(proj i) . y = xi