theorem Th1: :: LOPBAN10:1

for X being non-empty non empty FinSequence
for x being Element of product X
for i being Element of dom X
for r being object st r in X . i holds
((reproj (i,x)) . r) . i = r