let 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 holds
(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)
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 holds
(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)
let G be Go-board; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies (left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: f is_sequence_on G ; :: thesis: (left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)
k + 1 >= 1 by NAT_1:11;
then A4: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A5: [i2,j2] in Indices G and
A6: f /. (k + 1) = G * (i2,j2) by A3, GOBOARD1:def 9;
A7: 1 <= j2 by A5, MATRIX_0:32;
A8: i2 <= len G by A5, MATRIX_0:32;
A9: 1 <= i2 by A5, MATRIX_0:32;
A10: j2 <= width G by A5, MATRIX_0:32;
k <= k + 1 by NAT_1:11;
then k <= len f by A2, XXREAL_0:2;
then A11: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A12: [i1,j1] in Indices G and
A13: f /. k = G * (i1,j1) by A3, GOBOARD1:def 9;
A14: 0 + 1 <= j1 by A12, MATRIX_0:32;
then j1 > 0 ;
then consider j being Nat such that
A15: j + 1 = j1 by NAT_1:6;
A16: |.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A11, A12, A13, A4, A5, A6, GOBOARD1:def 9;
A22: j1 -' 1 = j by A15, NAT_D:34;
A23: j1 <= width G by A12, MATRIX_0:32;
then A24: j < width G by A15, NAT_1:13;
A25: 0 + 1 <= i1 by A12, MATRIX_0:32;
then i1 > 0 ;
then consider i being Nat such that
A26: i + 1 = i1 by NAT_1:6;
A27: i1 <= len G by A12, MATRIX_0:32;
then A28: i < len G by A26, NAT_1:13;
A29: i1 -' 1 = i by A26, NAT_D:34;
reconsider i = i, j = j as Nat ;