let i, j, k be 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] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

right_cell (f,k,G) = cell (G,i,(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] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

right_cell (f,k,G) = cell (G,i,(j -' 1))

let G be Go-board; :: thesis: ( 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,j) & f /. (k + 1) = G * ((i + 1),j) implies right_cell (f,k,G) = cell (G,i,(j -' 1)) )

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,j) & f /. (k + 1) = G * ((i + 1),j) ) ; :: thesis: right_cell (f,k,G) = cell (G,i,(j -' 1))

hence right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, Def1; :: thesis: verum

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,j) & f /. (k + 1) = G * ((i + 1),j) holds

right_cell (f,k,G) = cell (G,i,(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] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

right_cell (f,k,G) = cell (G,i,(j -' 1))

let G be Go-board; :: thesis: ( 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,j) & f /. (k + 1) = G * ((i + 1),j) implies right_cell (f,k,G) = cell (G,i,(j -' 1)) )

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,j) & f /. (k + 1) = G * ((i + 1),j) ) ; :: thesis: right_cell (f,k,G) = cell (G,i,(j -' 1))

hence right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, Def1; :: thesis: verum