for X being RealNormSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for s being Function st x = s holds
(reproj (i,x)) . (s . i) = x