:: deftheorem Def5 defines reproj PDIFF_1:def 5 :
for i being Nat
for x being FinSequence of REAL
for b₃ being Function holds
( b₃ = reproj (i,x) iff ( dom b₃ = REAL & ( for r being Element of REAL holds b₃ . r = Replace (x,i,r) ) ) );