:: deftheorem Def6 defines proj2 PSCOMP_1:def 6 :
for b₁ being RealMap of (TOP-REAL 2) holds
( b₁ = proj2 iff for p being Point of (TOP-REAL 2) holds b₁ . p = p `2 );