:: deftheorem Def1 defines X_axis GOBOARD1:def 1 :
for f being FinSequence of (TOP-REAL 2)
for b₂ being FinSequence of REAL holds
( b₂ = X_axis f iff ( len b₂ = len f & ( for n being Nat st n in dom b₂ holds
b₂ . n = (f /. n) `1 ) ) );