theorem NDIFF5def4: :: LOPBAN12:2

for G being RealLinearSpace-Sequence
for i being Element of dom G
for x being Element of (product G)
for r being Element of (G . i) holds (reproj (i,x)) . r = x +* (i,r)