theorem Th30: :: GOBOARD5:30

for i, j, k being Nat
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) holds
( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) )