:: deftheorem Def1 defines diffX2_1 JORDAN:def 1 :
for o being Point of (TOP-REAL 2)
for b₂ being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b₂ = diffX2_1 o iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b₂ . x = ((x `2) `1) - (o `1) );