let f be non empty standard FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * m,k & f /. (n + 1) = (GoB f) * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
let n be Element of NAT ; :: thesis: ( n in dom f & n + 1 in dom f implies for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * m,k & f /. (n + 1) = (GoB f) * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume A1: ( n in dom f & n + 1 in dom f ) ; :: thesis: for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * m,k & f /. (n + 1) = (GoB f) * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
f is_sequence_on GoB f by Def5;
hence for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * m,k & f /. (n + 1) = (GoB f) * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by A1, GOBOARD1:def 11; :: thesis: verum