let n be Element of NAT ; :: thesis:
let G be Go-board; :: thesis:
let f be standard special_circular_sequence; :: thesis:
assume that
A1: ( 1 <= n & n + 1 <= len f ) and
A2: f is_sequence_on G ; :: thesis:
set F = GoB f;
A3: Values (GoB f) c= Values G by A2, Th21;
f is_sequence_on GoB f by GOBOARD5:def 5;
then consider m, k, i, j being Element of NAT such that
A4: [m,k] in Indices (GoB f) and
A5: f /. n = (GoB f) * m,k and
A6: [i,j] in Indices (GoB f) and
A7: f /. (n + 1) = (GoB f) * i,j and
( ( m = i & k + 1 = j ) or ( m + 1 = i & k = j ) or ( m = i + 1 & k = j ) or ( m = i & k = j + 1 ) ) by A1, JORDAN8:6;
A8: ( 1 <= m & m <= len (GoB f) & 1 <= k & k <= width (GoB f) ) by A4, MATRIX_1:39;
A9: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) ) by A6, MATRIX_1:39;
then A10: ( ((GoB f) * i,j) `1 = ((GoB f) * i,1) `1 & ((GoB f) * i,k) `1 = ((GoB f) * i,1) `1 ) by A8, GOBOARD5:3;
A11: ( ((GoB f) * i,j) `2 = ((GoB f) * 1,j) `2 & ((GoB f) * m,j) `2 = ((GoB f) * 1,j) `2 ) by A8, A9, GOBOARD5:2;
consider i1, j1, i2, j2 being Element of NAT such that
A12: [i1,j1] in Indices G and
A13: f /. n = G * i1,j1 and
A14: [i2,j2] in Indices G and
A15: f /. (n + 1) = G * i2,j2 and
A16: ( ( 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;
A17: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G ) by A12, MATRIX_1:39;
A18: ( 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A14, MATRIX_1:39;
then A19: ( (G * i1,j1) `1 = (G * i1,1) `1 & (G * i2,j2) `1 = (G * i2,1) `1 ) by A17, GOBOARD5:3;
A20: ( (G * i1,j1) `2 = (G * 1,j1) `2 & (G * i2,j1) `2 = (G * 1,j1) `2 ) by A17, A18, GOBOARD5:2;
A21: ( k + 1 >= 1 & j + 1 >= 1 & m + 1 >= 1 & i + 1 >= 1 ) by NAT_1:12;
A22: ( k + 1 > k & j + 1 > j & m + 1 > m & i + 1 > i ) by NAT_1:13;
A23: ( i1 + 1 > i1 & j1 + 1 > j1 & i2 + 1 > i2 & j2 + 1 > j2 ) by NAT_1:13;

per cases by A16;

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

now

assume j <= k ; :: thesis:
then A25: ((GoB f) * i,j) `2 <= ((GoB f) * m,k) `2 by A8, A9, A11, SPRECT_3:24;
j1 < j2 by A24, NAT_1:13;
hence contradiction by A5, A7, A13, A15, A17, A18, A20, A25, GOBOARD5:5; :: thesis:

end;

then A26: k + 1 <= j by NAT_1:13;

now

assume A27: k + 1 < j ; :: thesis:
then A28: k + 1 < width (GoB f) by A9, XXREAL_0:2;
then consider l, i' being Element of NAT such that
A29: l in dom f and
A30: [i',(k + 1)] in Indices (GoB f) and
A31: f /. l = (GoB f) * i',(k + 1) by A21, JORDAN5D:10;
( 1 <= i' & i' <= len (GoB f) ) by A30, MATRIX_1:39;
then A32: ( ((GoB f) * i',(k + 1)) `2 = ((GoB f) * 1,(k + 1)) `2 & ((GoB f) * m,(k + 1)) `2 = ((GoB f) * 1,(k + 1)) `2 ) by A8, A21, A28, GOBOARD5:2;
consider i1', j1' being Element of NAT such that
A33: [i1',j1'] in Indices G and
A34: f /. l = G * i1',j1' by A2, A29, GOBOARD1:def 11;
A35: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A33, MATRIX_1:39;
then A36: ( (G * i1',j1') `2 = (G * 1,j1') `2 & (G * i1',j1) `2 = (G * 1,j1) `2 ) by A17, GOBOARD5:2;
A37: ( (G * i2,j2) `2 = (G * 1,j2) `2 & (G * i1',j2) `2 = (G * 1,j2) `2 ) by A18, A35, GOBOARD5:2;

A38: now

assume j1 >= j1' ; :: thesis:
then (G * i1',j1') `2 <= (G * i1,j1) `2 by A17, A20, A35, A36, SPRECT_3:24;
hence contradiction by A5, A8, A13, A22, A28, A31, A32, A34, GOBOARD5:5; :: thesis:

end;

now

assume j2 <= j1' ; :: thesis:
then (G * i2,j2) `2 <= (G * i1',j1') `2 by A18, A35, A37, SPRECT_3:24;
hence contradiction by A7, A8, A9, A11, A15, A21, A27, A31, A32, A34, GOBOARD5:5; :: thesis:

end;

hence contradiction by A24, A38, NAT_1:13; :: thesis:

end;

then A39: k + 1 = j by A26, XXREAL_0:1;
then A40: ( right_cell f,n,G = cell G,i1,j1 & right_cell f,n = cell (GoB f),m,k ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A24, Def2, GOBOARD5:def 6;
( left_cell f,n,G = cell G,(i1 -' 1),j1 & left_cell f,n = cell (GoB f),(m -' 1),k ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A24, A39, Def3, GOBOARD5:def 7;
hence ( left_cell f,n,G c= left_cell f,n & right_cell f,n,G c= right_cell f,n ) by A3, A4, A5, A12, A13, A40, Th18, Th19; :: thesis:

end;

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

now

assume i <= m ; :: thesis:
then A42: ((GoB f) * i,j) `1 <= ((GoB f) * m,k) `1 by A8, A9, A10, SPRECT_3:25;
i1 < i2 by A41, NAT_1:13;
hence contradiction by A5, A7, A13, A15, A17, A18, A41, A42, GOBOARD5:4; :: thesis:

end;

then A43: m + 1 <= i by NAT_1:13;

now

assume A44: m + 1 < i ; :: thesis:
then A45: m + 1 < len (GoB f) by A9, XXREAL_0:2;
then consider l, j' being Element of NAT such that
A46: l in dom f and
A47: [(m + 1),j'] in Indices (GoB f) and
A48: f /. l = (GoB f) * (m + 1),j' by A21, JORDAN5D:9;
A49: 1 <= m + 1 by NAT_1:12;
( 1 <= j' & j' <= width (GoB f) ) by A47, MATRIX_1:39;
then A50: ( ((GoB f) * (m + 1),j') `1 = ((GoB f) * (m + 1),1) `1 & ((GoB f) * (m + 1),k) `1 = ((GoB f) * (m + 1),1) `1 ) by A8, A21, A45, GOBOARD5:3;
A51: ( ((GoB f) * (m + 1),j) `1 = ((GoB f) * (m + 1),1) `1 & ((GoB f) * (m + 1),k) `1 = ((GoB f) * (m + 1),1) `1 ) by A8, A9, A21, A45, GOBOARD5:3;
consider i1', j1' being Element of NAT such that
A52: [i1',j1'] in Indices G and
A53: f /. l = G * i1',j1' by A2, A46, GOBOARD1:def 11;
A54: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A52, MATRIX_1:39;
then A55: ( (G * i1',j1') `1 = (G * i1',1) `1 & (G * i1',j1) `1 = (G * i1',1) `1 ) by A17, GOBOARD5:3;
A56: ( (G * i2,j2) `1 = (G * i2,1) `1 & (G * i2,j1') `1 = (G * i2,1) `1 ) by A18, A54, GOBOARD5:3;

A57: now

assume i1 >= i1' ; :: thesis:
then (G * i1',j1') `1 <= (G * i1,j1) `1 by A17, A54, A55, SPRECT_3:25;
hence contradiction by A5, A8, A13, A22, A45, A48, A50, A53, GOBOARD5:4; :: thesis:

end;

now

assume i2 <= i1' ; :: thesis:
then (G * i2,j2) `1 <= (G * i1',j1') `1 by A18, A54, A56, SPRECT_3:25;
hence contradiction by A7, A9, A15, A44, A48, A49, A50, A51, A53, GOBOARD5:4; :: thesis:

end;

hence contradiction by A41, A57, NAT_1:13; :: thesis:

end;

then A58: m + 1 = i by A43, XXREAL_0:1;
then A59: ( right_cell f,n,G = cell G,i1,(j1 -' 1) & right_cell f,n = cell (GoB f),m,(k -' 1) ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A41, Def2, GOBOARD5:def 6;
( left_cell f,n,G = cell G,i1,j1 & left_cell f,n = cell (GoB f),m,k ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A41, A58, Def3, GOBOARD5:def 7;
hence ( left_cell f,n,G c= left_cell f,n & right_cell f,n,G c= right_cell f,n ) by A3, A4, A5, A12, A13, A59, Th18, Th20; :: thesis:

end;

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

now

assume m <= i ; :: thesis:
then A61: ((GoB f) * i,j) `1 >= ((GoB f) * m,k) `1 by A8, A9, A10, SPRECT_3:25;
i1 > i2 by A60, NAT_1:13;
hence contradiction by A5, A7, A13, A15, A17, A18, A60, A61, GOBOARD5:4; :: thesis:

end;

then A62: i + 1 <= m by NAT_1:13;

now

assume A63: m > i + 1 ; :: thesis:
then A64: i + 1 < len (GoB f) by A8, XXREAL_0:2;
then consider l, j' being Element of NAT such that
A65: l in dom f and
A66: [(i + 1),j'] in Indices (GoB f) and
A67: f /. l = (GoB f) * (i + 1),j' by A21, JORDAN5D:9;
A68: 1 <= i + 1 by NAT_1:12;
( 1 <= j' & j' <= width (GoB f) ) by A66, MATRIX_1:39;
then A69: ( ((GoB f) * (i + 1),j') `1 = ((GoB f) * (i + 1),1) `1 & ((GoB f) * (i + 1),j) `1 = ((GoB f) * (i + 1),1) `1 ) by A9, A21, A64, GOBOARD5:3;
A70: ( ((GoB f) * (i + 1),j) `1 = ((GoB f) * (i + 1),1) `1 & ((GoB f) * (i + 1),k) `1 = ((GoB f) * (i + 1),1) `1 ) by A8, A9, A21, A64, GOBOARD5:3;
consider i1', j1' being Element of NAT such that
A71: [i1',j1'] in Indices G and
A72: f /. l = G * i1',j1' by A2, A65, GOBOARD1:def 11;
A73: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A71, MATRIX_1:39;
then A74: ( (G * i1',j1') `1 = (G * i1',1) `1 & (G * i1',j1) `1 = (G * i1',1) `1 ) by A17, GOBOARD5:3;
A75: ( (G * i2,j2) `1 = (G * i2,1) `1 & (G * i2,j1') `1 = (G * i2,1) `1 ) by A18, A73, GOBOARD5:3;

A76: now

assume i2 >= i1' ; :: thesis:
then (G * i2,j2) `1 >= (G * i1',j1') `1 by A18, A73, A75, SPRECT_3:25;
hence contradiction by A7, A9, A15, A22, A64, A67, A69, A72, GOBOARD5:4; :: thesis:

end;

now

assume i1 <= i1' ; :: thesis:
then (G * i1',j1') `1 >= (G * i1,j1) `1 by A17, A73, A74, SPRECT_3:25;
hence contradiction by A5, A8, A13, A63, A67, A68, A69, A70, A72, GOBOARD5:4; :: thesis:

end;

hence contradiction by A60, A76, NAT_1:13; :: thesis:

end;

then A77: i + 1 = m by A62, XXREAL_0:1;
then A78: ( right_cell f,n,G = cell G,i2,j2 & right_cell f,n = cell (GoB f),i,j ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A60, Def2, GOBOARD5:def 6;
( left_cell f,n,G = cell G,i2,(j2 -' 1) & left_cell f,n = cell (GoB f),i,(j -' 1) ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A60, A77, Def3, GOBOARD5:def 7;
hence ( left_cell f,n,G c= left_cell f,n & right_cell f,n,G c= right_cell f,n ) by A3, A6, A7, A14, A15, A78, Th18, Th20; :: thesis:

end;

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

A80: now

assume A81: m <> i ; :: thesis:

per cases by A81, XXREAL_0:1;

suppose m < i ; :: thesis:

hence contradiction by A5, A7, A8, A9, A10, A13, A15, A19, A79, GOBOARD5:4; :: thesis:

end;

suppose m > i ; :: thesis:

hence contradiction by A5, A7, A8, A9, A10, A13, A15, A19, A79, GOBOARD5:4; :: thesis:

end;

now

assume j >= k ; :: thesis:
then A82: ((GoB f) * i,j) `2 >= ((GoB f) * m,k) `2 by A8, A9, A11, SPRECT_3:24;
j1 > j2 by A79, NAT_1:13;
hence contradiction by A5, A7, A13, A15, A17, A18, A20, A82, GOBOARD5:5; :: thesis:

end;

then A83: j + 1 <= k by NAT_1:13;

now

assume A84: j + 1 < k ; :: thesis:
then A85: j + 1 < width (GoB f) by A8, XXREAL_0:2;
then consider l, i' being Element of NAT such that
A86: l in dom f and
A87: [i',(j + 1)] in Indices (GoB f) and
A88: f /. l = (GoB f) * i',(j + 1) by A21, JORDAN5D:10;
( 1 <= i' & i' <= len (GoB f) ) by A87, MATRIX_1:39;
then A89: ( ((GoB f) * i',(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 & ((GoB f) * i,(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 ) by A9, A21, A85, GOBOARD5:2;
A90: ( ((GoB f) * i,(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 & ((GoB f) * m,(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 ) by A8, A9, A21, A85, GOBOARD5:2;
consider i1', j1' being Element of NAT such that
A91: [i1',j1'] in Indices G and
A92: f /. l = G * i1',j1' by A2, A86, GOBOARD1:def 11;
A93: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A91, MATRIX_1:39;
then A94: ( (G * i1',j1') `2 = (G * 1,j1') `2 & (G * i1',j1) `2 = (G * 1,j1) `2 ) by A17, GOBOARD5:2;
A95: ( (G * i2,j2) `2 = (G * 1,j2) `2 & (G * i1',j2) `2 = (G * 1,j2) `2 ) by A18, A93, GOBOARD5:2;

A96: now

assume j2 >= j1' ; :: thesis:
then (G * i2,j2) `2 >= (G * i1',j1') `2 by A18, A93, A95, SPRECT_3:24;
hence contradiction by A7, A9, A15, A22, A85, A88, A89, A92, GOBOARD5:5; :: thesis:

end;

now

assume j1 <= j1' ; :: thesis:
then (G * i1',j1') `2 >= (G * i1,j1) `2 by A17, A20, A93, A94, SPRECT_3:24;
hence contradiction by A5, A8, A13, A21, A84, A88, A89, A90, A92, GOBOARD5:5; :: thesis:

end;

hence contradiction by A79, A96, NAT_1:13; :: thesis:

end;

then A97: j + 1 = k by A83, XXREAL_0:1;
then A98: ( right_cell f,n,G = cell G,(i1 -' 1),j2 & right_cell f,n = cell (GoB f),(m -' 1),j ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A79, Def2, GOBOARD5:def 6;
( left_cell f,n,G = cell G,i1,j2 & left_cell f,n = cell (GoB f),m,j ) by A1, A2, A4, A5, A6, A7, A12, A13, A14, A15, A22, A23, A79, A97, Def3, GOBOARD5:def 7;
hence ( left_cell f,n,G c= left_cell f,n & right_cell f,n,G c= right_cell f,n ) by A3, A6, A7, A14, A15, A79, A80, A98, Th18, Th19; :: thesis:

end;