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