theorem :: GOBRD13:41

for i, j, k being Nat
for f being FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
front_right_cell (f,k,G) = cell (G,(i -' 1),(j -' 1))