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] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j holds
left_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 + 1),j & f /. (k + 1) = G * i,j holds
left_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 + 1),j & f /. (k + 1) = G * i,j implies left_cell f,k,G = cell G,i,(j -' 1) )
assume that
A1: ( 1 <= k & k + 1 <= len f ) and
A2: f is_sequence_on G and
A3: ( [i,j] in Indices G & [(i + 1),j] in Indices G ) and
A4: f /. k = G * (i + 1),j and
A5: f /. (k + 1) = G * i,j ; :: thesis: left_cell f,k,G = cell G,i,(j -' 1)
A6: i < i + 1 by XREAL_1:31;
i + 1 <= (i + 1) + 1 by NAT_1:11;
hence left_cell f,k,G = cell G,i,(j -' 1) by A1, A2, A3, A4, A5, A6, Def3; :: thesis: verum