:: deftheorem Def1 defines reproj LOPBAN10:def 1 :
for X being non-empty non empty FinSequence
for i being object
for x being Element of product X
for b₄ being Function of (X . i),(product X) holds
( b₄ = reproj (i,x) iff for r being object st r in X . i holds
b₄ . r = x +* (i,r) );