:: deftheorem Def20 defines reproj LOPBAN10:def 2 :
for X being RealLinearSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for b₄ being Function of (X . i),(product X) holds
( b₄ = reproj (i,x) iff ex x0 being Element of product (carr X) st
( x0 = x & b₄ = reproj (i,x0) ) );