:: deftheorem Def4 defines Proj PDIFF_1:def 4 :
for i, n being Nat
for b₃ being Function of (REAL-NS n),(REAL-NS 1) holds
( b₃ = Proj (i,n) iff for x being Point of (REAL-NS n) holds b₃ . x = <*((proj (i,n)) . x)*> );