let i, j, k be 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] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
front_right_cell (f,k,G) = cell (G,(i -' 1),j)
let f be FinSequence of (TOP-REAL 2); for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds
front_right_cell (f,k,G) = cell (G,(i -' 1),j)
let G be Go-board; ( 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) implies front_right_cell (f,k,G) = cell (G,(i -' 1),j) )
A1:
( i < i + 1 & i + 1 <= (i + 1) + 1 )
by XREAL_1:29;
assume
( 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) )
; front_right_cell (f,k,G) = cell (G,(i -' 1),j)
hence
front_right_cell (f,k,G) = cell (G,(i -' 1),j)
by A1, Def3; verum