theorem :: GOBOARD1:24

for f1, f2 being FinSequence of (TOP-REAL 2)
for D being set
for M being Matrix of D st ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * (m,k) & f2 /. 1 = M * (i,j) & len f1 in dom f1 & 1 in dom f2 holds
|.(m - i).| + |.(k - j).| = 1 ) holds
for n being Nat st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1