let k 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 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:27;
then consider i2, j2 being Element of NAT such that
A5: [i2,j2] in Indices G and
A6: f /. (k + 1) = G * i2,j2 by A3, GOBOARD1:def 11;
A7: 1 <= j2 by A5, MATRIX_1:39;
A8: i2 <= len G by A5, MATRIX_1:39;
A9: 1 <= i2 by A5, MATRIX_1:39;
A10: j2 <= width G by A5, MATRIX_1:39;
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:27;
then consider i1, j1 being Element of NAT such that
A12: [i1,j1] in Indices G and
A13: f /. k = G * i1,j1 by A3, GOBOARD1:def 11;
A14: 0 + 1 <= j1 by A12, MATRIX_1:39;
then j1 > 0 by NAT_1:13;
then consider j being Nat such that
A15: j + 1 = j1 by NAT_1:6;
A16: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A11, A12, A13, A4, A5, A6, GOBOARD1:def 11;

A17: now

per cases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A16, SEQM_3:82;

case that A18: abs (i1 - i2) = 1 and
A19: j1 = j2 ; :: thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )

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

end;

case that A20: i1 = i2 and
A21: abs (j1 - j2) = 1 ; :: thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )

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

end;

end;

end;

A22: j1 -' 1 = j by A15, NAT_D:34;
A23: j1 <= width G by A12, MATRIX_1:39;
then A24: j < width G by A15, NAT_1:13;
A25: 0 + 1 <= i1 by A12, MATRIX_1:39;
then i1 > 0 by NAT_1:13;
then consider i being Nat such that
A26: i + 1 = i1 by NAT_1:6;
A27: i1 <= len G by A12, MATRIX_1:39;
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 Element of NAT by ORDINAL1:def 13;

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

suppose A30: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg f,k

then A31: right_cell f,k,G = cell G,i1,j1 by A1, A2, A3, A12, A13, A5, A6, Th23;
( j1 < width G & left_cell f,k,G = cell G,i,j1 ) by A1, A2, A3, A12, A13, A5, A6, A10, A29, A30, Th22, NAT_1:13;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * i1,j1),(G * i1,(j1 + 1)) by A14, A26, A28, A31, GOBOARD5:26
.= LSeg f,k by A1, A2, A13, A6, A30, TOPREAL1:def 5 ;
:: thesis: verum

end;

suppose A32: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg f,k

then A33: right_cell f,k,G = cell G,i1,j by A1, A2, A3, A12, A13, A5, A6, A22, Th25;
( i1 < len G & left_cell f,k,G = cell G,i1,j1 ) by A1, A2, A3, A12, A13, A5, A6, A8, A32, Th24, NAT_1:13;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * i1,j1),(G * (i1 + 1),j1) by A25, A15, A24, A33, GOBOARD5:27
.= LSeg f,k by A1, A2, A13, A6, A32, TOPREAL1:def 5 ;
:: thesis: verum

end;

suppose A34: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg f,k

then A35: right_cell f,k,G = cell G,i2,j1 by A1, A2, A3, A12, A13, A5, A6, Th27;
( i2 < len G & left_cell f,k,G = cell G,i2,j ) by A1, A2, A3, A12, A13, A5, A6, A27, A22, A34, Th26, NAT_1:13;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * (i2 + 1),j1),(G * i2,j1) by A9, A15, A24, A35, GOBOARD5:27
.= LSeg f,k by A1, A2, A13, A6, A34, TOPREAL1:def 5 ;
:: thesis: verum

end;

suppose A36: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg f,k

then A37: right_cell f,k,G = cell G,i,j2 by A1, A2, A3, A12, A13, A5, A6, A29, Th29;
( j2 < width G & left_cell f,k,G = cell G,i1,j2 ) by A1, A2, A3, A12, A13, A5, A6, A23, A36, Th28, NAT_1:13;
hence (left_cell f,k,G) /\ (right_cell f,k,G) = LSeg (G * i1,(j2 + 1)),(G * i1,j2) by A7, A26, A28, A37, GOBOARD5:26
.= LSeg f,k by A1, A2, A13, A6, A36, TOPREAL1:def 5 ;
:: thesis: verum

end;

end;