theorem :: GOBOARD7:52

for i, j, k being Nat
for f being constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,j) & f /. (k + 1) = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) )