let k be Element of NAT ; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
let G be Go-board; :: thesis:
assume that
A1: ( 1 <= k & k + 1 <= len f ) and
A2: f is_sequence_on G ; :: thesis:
k <= k + 1 by NAT_1:11;
then k <= len f by A1, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A4: ( [i1,j1] in Indices G & f /. k = G * i1,j1 ) by A2, GOBOARD1:def 11;
k + 1 >= 1 by NAT_1:11;
then A5: k + 1 in dom f by A1, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A6: ( [i2,j2] in Indices G & f /. (k + 1) = G * i2,j2 ) by A2, GOBOARD1:def 11;
A7: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A3, A4, A5, A6, GOBOARD1:def 11;

A8: now

per cases by A7, GOBOARD1:2;

case that A9: abs (i1 - i2) = 1 and
A10: j1 = j2 ; :: thesis:

( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A9, ABSVALUE:def 1;
hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; :: thesis:
thus j1 = j2 by A10; :: thesis:

end;

case that A11: i1 = i2 and
A12: abs (j1 - j2) = 1 ; :: thesis:

( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A12, ABSVALUE:def 1;
hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; :: thesis:
thus i1 = i2 by A11; :: thesis:

end;

A13: ( 0 + 1 <= j1 & j1 <= width G ) by A4, MATRIX_1:39;
A14: ( 1 <= j2 & j2 <= width G ) by A6, MATRIX_1:39;
A15: ( 0 + 1 <= i1 & i1 <= len G ) by A4, MATRIX_1:39;
A16: ( 1 <= i2 & i2 <= len G ) by A6, MATRIX_1:39;
i1 > 0 by A15, NAT_1:13;
then consider i being Nat such that
A17: i + 1 = i1 by NAT_1:6;
A18: i < len G by A15, A17, NAT_1:13;
j1 > 0 by A13, NAT_1:13;
then consider j being Nat such that
A19: j + 1 = j1 by NAT_1:6;
A20: j < width G by A13, A19, NAT_1:13;
A21: ( i1 -' 1 = i & j1 -' 1 = j ) by A17, A19, NAT_D:34;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 13;

per cases by A8;

suppose A22: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then A23: j1 < width G by A14, NAT_1:13;
( left_cell f,k,G = cell G,i,j1 & right_cell f,k,G = cell G,i1,j1 ) by A1, A2, A4, A6, A21, A22, Th22, Th23;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * i1,j1),(G * i1,(j1 + 1)) by A13, A17, A18, A23, GOBOARD5:26
.= LSeg f,k by A1, A4, A6, A22, TOPREAL1:def 5 ;
:: thesis:

end;

suppose A24: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then A25: i1 < len G by A16, NAT_1:13;
( left_cell f,k,G = cell G,i1,j1 & right_cell f,k,G = cell G,i1,j ) by A1, A2, A4, A6, A21, A24, Th24, Th25;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * i1,j1),(G * (i1 + 1),j1) by A15, A19, A20, A25, GOBOARD5:27
.= LSeg f,k by A1, A4, A6, A24, TOPREAL1:def 5 ;
:: thesis:

end;

suppose A26: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then A27: i2 < len G by A15, NAT_1:13;
( left_cell f,k,G = cell G,i2,j & right_cell f,k,G = cell G,i2,j1 ) by A1, A2, A4, A6, A21, A26, Th26, Th27;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * (i2 + 1),j1),(G * i2,j1) by A16, A19, A20, A27, GOBOARD5:27
.= LSeg f,k by A1, A4, A6, A26, TOPREAL1:def 5 ;
:: thesis:

end;

suppose A28: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then A29: j2 < width G by A13, NAT_1:13;
( left_cell f,k,G = cell G,i1,j2 & right_cell f,k,G = cell G,i,j2 ) by A1, A2, A4, A6, A21, A28, Th28, Th29;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * i1,(j2 + 1)),(G * i1,j2) by A14, A17, A18, A29, GOBOARD5:26
.= LSeg f,k by A1, A4, A6, A28, TOPREAL1:def 5 ;
:: thesis:

end;