:: deftheorem defines is_sequence_on GOBOARD1:def 9 :
for D being set
for f being FinSequence of D
for M being Matrix of D holds
( f is_sequence_on M iff ( ( for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) ) );