let i, j, k be Nat; :: thesis: for f being FinSequence of ()
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
right_cell (f,k,G) = cell (G,i,j)

let f be FinSequence of (); :: thesis: for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
right_cell (f,k,G) = cell (G,i,j)

let G be Go-board; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) implies right_cell (f,k,G) = cell (G,i,j) )
A1: ( j < j + 1 & j + 1 <= (j + 1) + 1 ) by XREAL_1:29;
assume ( 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) ; :: thesis: right_cell (f,k,G) = cell (G,i,j)
hence right_cell (f,k,G) = cell (G,i,j) by ; :: thesis: verum