:: deftheorem Def6 defines reproj PDIFF_1:def 6 :
for n, i being Nat
for x being Point of (REAL-NS n)
for b₄ being Function of (REAL-NS 1),(REAL-NS n) holds
( b₄ = reproj (i,x) iff for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b₄ . r = (reproj (i,y)) . q ) );