theorem Th4: :: LOPBAN10:5

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