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