theorem Th48: :: NDIFF_5:48

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
reproj (i,x) = reproj (i,y)