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 & 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 & k + 1 <= len f ) and
A2: f is_sequence_on G and
A3: 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:79; :: thesis: verum

end;

suppose A4: 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 )

consider i1, j1, i2, j2 being Element of NAT such that
A5: ( [i1,j1] in Indices G & f /. k = G * i1,j1 ) and
A6: ( [i2,j2] in Indices G & f /. (k + 1) = G * i2,j2 ) and
A7: ( ( 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;
A8: ( i1 + 1 > i1 & i2 + 1 > i2 & j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
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;
A9: f | n is_sequence_on G by A2, GOBOARD1:38;
A10: len (f | n) = n by A4, FINSEQ_1:80;
then ( k in dom (f | n) & k + 1 in dom (f | n) ) by A1, A3, GOBOARD2:3;
then A11: ( (f | n) /. k = f /. k & (f | n) /. (k + 1) = f /. (k + 1) ) by FINSEQ_4:85;

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

suppose A12: ( 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, A5, A6, A8, Def5
.= front_left_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A12, Def5 ;
:: 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, A5, A6, A8, A12, Def4
.= front_right_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A12, Def4 ; :: thesis: verum

end;

suppose A13: ( 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, A5, A6, A8, Def5
.= front_left_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A13, Def5 ;
:: 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, A5, A6, A8, A13, Def4
.= front_right_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A13, Def4 ; :: thesis: verum

end;

suppose A14: ( 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, A5, A6, A8, Def5
.= front_left_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A14, Def5 ;
:: 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, A5, A6, A8, A14, Def4
.= front_right_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A14, Def4 ; :: thesis: verum

end;

suppose A15: ( 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, A5, A6, A8, Def5
.= front_left_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A15, Def5 ;
:: 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, A5, A6, A8, A15, Def4
.= front_right_cell (f | n),k,G by A1, A3, A5, A6, A8, A9, A10, A11, A15, Def4 ; :: 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;