let k, n 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 /^ n) & n <= len f & f is_sequence_on G holds
( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )
let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G holds
( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )
let G be Go-board; :: thesis: ( 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G implies ( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G ) )
set g = f /^ n;
assume that
A1: 1 <= k and
A2: k + 1 <= len (f /^ n) and
A3: n <= len f and
A4: f is_sequence_on G ; :: thesis: ( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )
A5: ( len (f /^ n) = (len f) - n & (k + 1) + n <= (len (f /^ n)) + n ) by A2, A3, RFINSEQ:def 2, XREAL_1:8;
k in dom (f /^ n) by A1, A2, SEQ_4:151;
then A6: (f /^ n) /. k = f /. (k + n) by FINSEQ_5:30;
set lf = left_cell f,(k + n),G;
set lfn = left_cell (f /^ n),k,G;
set rf = right_cell f,(k + n),G;
set rfn = right_cell (f /^ n),k,G;
A7: ( (k + 1) + n = (k + n) + 1 & 1 <= k + n ) by A1, NAT_1:12;
k + 1 in dom (f /^ n) by A1, A2, SEQ_4:151;
then A8: (f /^ n) /. (k + 1) = f /. ((k + 1) + n) by FINSEQ_5:30;
A9: f /^ n is_sequence_on G by A4, JORDAN8:5;
then consider i1, j1, i2, j2 being Element of NAT such that
A10: ( [i1,j1] in Indices G & (f /^ n) /. k = G * i1,j1 & [i2,j2] in Indices G & (f /^ n) /. (k + 1) = G * i2,j2 ) and
A11: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, JORDAN8:6;
A12: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A13: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;

now

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A11;

suppose A14: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )

hence left_cell f,(k + n),G = cell G,(i1 -' 1),j1 by A4, A10, A12, A6, A8, A5, A7, Def3
.= left_cell (f /^ n),k,G by A1, A2, A9, A10, A12, A14, Def3 ;
:: thesis: right_cell f,(k + n),G = right_cell (f /^ n),k,G
thus right_cell f,(k + n),G = cell G,i1,j1 by A4, A10, A12, A6, A8, A5, A7, A14, Def2
.= right_cell (f /^ n),k,G by A1, A2, A9, A10, A12, A14, Def2 ; :: thesis: verum

end;

suppose A15: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )

hence left_cell f,(k + n),G = cell G,i1,j1 by A4, A10, A13, A6, A8, A5, A7, Def3
.= left_cell (f /^ n),k,G by A1, A2, A9, A10, A13, A15, Def3 ;
:: thesis: right_cell f,(k + n),G = right_cell (f /^ n),k,G
thus right_cell f,(k + n),G = cell G,i1,(j1 -' 1) by A4, A10, A13, A6, A8, A5, A7, A15, Def2
.= right_cell (f /^ n),k,G by A1, A2, A9, A10, A13, A15, Def2 ; :: thesis: verum

end;

suppose A16: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )

hence left_cell f,(k + n),G = cell G,i2,(j2 -' 1) by A4, A10, A13, A6, A8, A5, A7, Def3
.= left_cell (f /^ n),k,G by A1, A2, A9, A10, A13, A16, Def3 ;
:: thesis: right_cell f,(k + n),G = right_cell (f /^ n),k,G
thus right_cell f,(k + n),G = cell G,i2,j2 by A4, A10, A13, A6, A8, A5, A7, A16, Def2
.= right_cell (f /^ n),k,G by A1, A2, A9, A10, A13, A16, Def2 ; :: thesis: verum

end;

suppose A17: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )

hence left_cell f,(k + n),G = cell G,i1,j2 by A4, A10, A12, A6, A8, A5, A7, Def3
.= left_cell (f /^ n),k,G by A1, A2, A9, A10, A12, A17, Def3 ;
:: thesis: right_cell f,(k + n),G = right_cell (f /^ n),k,G
thus right_cell f,(k + n),G = cell G,(i1 -' 1),j2 by A4, A10, A12, A6, A8, A5, A7, A17, Def2
.= right_cell (f /^ n),k,G by A1, A2, A9, A10, A12, A17, Def2 ; :: thesis: verum

end;

end;

end;

hence ( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G ) ; :: thesis: verum