:: deftheorem Def6 defines Proj2_2 JORDAN:def 6 :
for b₁ being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b₁ = Proj2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b₁ . x = (x `2) `2 );