theorem Th3: :: LOPBAN10:4

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