:: deftheorem Def1 defines proj PDIFF_1:def 1 :
for i, n being Nat
for b₃ being Function of (REAL n),REAL holds
( b₃ = proj (i,n) iff for x being Element of REAL n holds b₃ . x = x . i );