theorem Th4X: :: LOPBAN10:6

for X being RealLinearSpace-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