:: deftheorem defines GoB GOBOARD2:def 2 :
for f being non empty FinSequence of (TOP-REAL 2) holds GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f)));