:: deftheorem Def4 defines reproj NDIFF_5:def 4 :
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Element of (product G)
for b₄ being Function of (G . i),(product G) holds
( b₄ = reproj (i,x) iff for r being Element of (G . i) holds b₄ . r = x +* (i,r) );