theorem Th47: :: NDIFF_5:47

for G being RealNormSpace-Sequence
for i being Element of dom G
for y being Point of (product G)
for q being Point of (G . i) st q = (proj i) . y holds
y = (reproj (i,y)) . q