let k, i, j be Element of NAT ; :: thesis: 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)
let f be FinSequence of (TOP-REAL 2); :: thesis: 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)
let G be Go-board; :: thesis: ( 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 implies front_right_cell f,k,G = cell G,(i -' 1),(j -' 1) )
A1: ( j < j + 1 & j + 1 <= (j + 1) + 1 ) by XREAL_1:31;
assume ( 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 ) ; :: thesis: front_right_cell f,k,G = cell G,(i -' 1),(j -' 1)
hence front_right_cell f,k,G = cell G,(i -' 1),(j -' 1) by A1, Def4; :: thesis: verum