:: deftheorem Def6 defines PROJ TOPREALC:def 6 :
for m, n being Nat
for b₃ being Function of (TOP-REAL m),R^1 holds
( b₃ = PROJ (m,n) iff for p being Element of (TOP-REAL m) holds b₃ . p = p /. n );