let f be non empty standard FinSequence of (TOP-REAL 2); :: thesis: 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 (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds
|.(m - i).| + |.(k - j).| = 1
let n be Nat; :: thesis: ( n in dom f & n + 1 in dom f implies for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 )
assume that
A1: n in dom f and
A2: n + 1 in dom f ; :: thesis: for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1
f is_sequence_on GoB f by Def5;
hence for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 by A1, A2; :: thesis: verum