let k, n 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 & k + 1 <= n holds
( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_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 & f is_sequence_on G & k + 1 <= n holds
( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )
let G be Go-board; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n implies ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: f is_sequence_on G and
A4: k + 1 <= n ; :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

per cases ( len f <= n or n < len f ) ;

suppose len f <= n ; :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

hence ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) ) by FINSEQ_1:58; :: thesis: verum

end;

suppose n < len f ; :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

then A5: len (f | n) = n by FINSEQ_1:59;
then k in dom (f | n) by A1, A4, SEQ_4:134;
then A6: (f | n) /. k = f /. k by FINSEQ_4:70;
k + 1 in dom (f | n) by A1, A4, A5, SEQ_4:134;
then A7: (f | n) /. (k + 1) = f /. (k + 1) by FINSEQ_4:70;
set lf = front_left_cell (f,k,G);
set lfn = front_left_cell ((f | n),k,G);
set rf = front_right_cell (f,k,G);
set rfn = front_right_cell ((f | n),k,G);
A8: f | n is_sequence_on G by A3, GOBOARD1:22;
consider i1, j1, i2, j2 being Nat such that
A9: ( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) ) and
A10: ( ( 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, A3, JORDAN8:3;
A11: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A12: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;

now :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

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 A10;

suppose A13: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

hence front_left_cell (f,k,G) = cell (G,(i2 -' 1),j2) by A1, A2, A3, A9, A11, Def4
.= front_left_cell ((f | n),k,G) by A1, A4, A9, A11, A8, A5, A6, A7, A13, Def4 ;
:: thesis: front_right_cell (f,k,G) = front_right_cell ((f | n),k,G)
thus front_right_cell (f,k,G) = cell (G,i2,j2) by A1, A2, A3, A9, A11, A13, Def3
.= front_right_cell ((f | n),k,G) by A1, A4, A9, A11, A8, A5, A6, A7, A13, Def3 ; :: thesis: verum

end;

suppose A14: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

hence front_left_cell (f,k,G) = cell (G,i2,j2) by A1, A2, A3, A9, A12, Def4
.= front_left_cell ((f | n),k,G) by A1, A4, A9, A12, A8, A5, A6, A7, A14, Def4 ;
:: thesis: front_right_cell (f,k,G) = front_right_cell ((f | n),k,G)
thus front_right_cell (f,k,G) = cell (G,i2,(j2 -' 1)) by A1, A2, A3, A9, A12, A14, Def3
.= front_right_cell ((f | n),k,G) by A1, A4, A9, A12, A8, A5, A6, A7, A14, Def3 ; :: thesis: verum

end;

suppose A15: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

hence front_left_cell (f,k,G) = cell (G,(i2 -' 1),(j2 -' 1)) by A1, A2, A3, A9, A12, Def4
.= front_left_cell ((f | n),k,G) by A1, A4, A9, A12, A8, A5, A6, A7, A15, Def4 ;
:: thesis: front_right_cell (f,k,G) = front_right_cell ((f | n),k,G)
thus front_right_cell (f,k,G) = cell (G,(i2 -' 1),j2) by A1, A2, A3, A9, A12, A15, Def3
.= front_right_cell ((f | n),k,G) by A1, A4, A9, A12, A8, A5, A6, A7, A15, Def3 ; :: thesis: verum

end;

suppose A16: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

hence front_left_cell (f,k,G) = cell (G,i2,(j2 -' 1)) by A1, A2, A3, A9, A11, Def4
.= front_left_cell ((f | n),k,G) by A1, A4, A9, A11, A8, A5, A6, A7, A16, Def4 ;
:: thesis: front_right_cell (f,k,G) = front_right_cell ((f | n),k,G)
thus front_right_cell (f,k,G) = cell (G,(i2 -' 1),(j2 -' 1)) by A1, A2, A3, A9, A11, A16, Def3
.= front_right_cell ((f | n),k,G) by A1, A4, A9, A11, A8, A5, A6, A7, A16, Def3 ; :: thesis: verum

end;

end;

end;

hence ( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) ) ; :: thesis: verum

end;

end;