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