let n be 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:
consider i1, j1, i2, j2 being Nat such that
A3: [i1,j1] in Indices G and
A4: f /. n = G * (i1,j1) and
A5: [i2,j2] in Indices G and
A6: f /. (n + 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:3;
A8: 1 <= j1 by A3, MATRIX_0:32;
A9: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A10: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;
A11: j2 <= width G by A5, MATRIX_0:32;
A12: j1 <= width G by A3, MATRIX_0:32;
A13: i2 <= len G by A5, MATRIX_0:32;
A14: 1 <= i2 by A5, MATRIX_0:32;
then A15: (G * (i2,j1)) `2 = (G * (1,j1)) `2 by A8, A12, A13, GOBOARD5:1;
A16: 1 <= j2 by A5, MATRIX_0:32;
then A17: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A14, A13, A11, GOBOARD5:2;
A18: i1 <= len G by A3, MATRIX_0:32;
set F = GoB f;
A19: Values (GoB f) c= Values G by A2, Th13;
f is_sequence_on GoB f by GOBOARD5:def 5;
then consider m, k, i, j being Nat such that
A20: [m,k] in Indices (GoB f) and
A21: f /. n = (GoB f) * (m,k) and
A22: [i,j] in Indices (GoB f) and
A23: 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:3;
A24: 1 <= m by A20, MATRIX_0:32;
A25: 1 <= i1 by A3, MATRIX_0:32;
then A26: (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A18, A8, A12, GOBOARD5:2;
A27: (G * (i1,j1)) `2 = (G * (1,j1)) `2 by A25, A18, A8, A12, GOBOARD5:1;
A28: m <= len (GoB f) by A20, MATRIX_0:32;
A29: j + 1 > j by NAT_1:13;
A30: k + 1 > k by NAT_1:13;
A31: k + 1 >= 1 by NAT_1:12;
A32: j + 1 >= 1 by NAT_1:12;
A33: j <= width (GoB f) by A22, MATRIX_0:32;
A34: i + 1 > i by NAT_1:13;
A35: m + 1 > m by NAT_1:13;
A36: i <= len (GoB f) by A22, MATRIX_0:32;
A37: i + 1 >= 1 by NAT_1:12;
A38: m + 1 >= 1 by NAT_1:12;
A39: k <= width (GoB f) by A20, MATRIX_0:32;
A40: 1 <= j by A22, MATRIX_0:32;
then A41: ((GoB f) * (m,j)) `2 = ((GoB f) * (1,j)) `2 by A24, A28, A33, GOBOARD5:1;
A42: 1 <= i by A22, MATRIX_0:32;
then A43: ((GoB f) * (i,j)) `1 = ((GoB f) * (i,1)) `1 by A36, A40, A33, GOBOARD5:2;
A44: ((GoB f) * (i,j)) `2 = ((GoB f) * (1,j)) `2 by A42, A36, A40, A33, GOBOARD5:1;
A45: 1 <= k by A20, MATRIX_0:32;
then A46: ((GoB f) * (i,k)) `1 = ((GoB f) * (i,1)) `1 by A39, A42, A36, GOBOARD5:2;

per cases by A7;

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

A48: now :: thesis:

A49: (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A14, A13, A16, A11, GOBOARD5:1;
assume A50: k + 1 < j ; :: thesis:
then A51: k + 1 < width (GoB f) by A33, XXREAL_0:2;
then consider l, i9 being Nat such that
A52: l in dom f and
A53: [i9,(k + 1)] in Indices (GoB f) and
A54: f /. l = (GoB f) * (i9,(k + 1)) by JORDAN5D:8, NAT_1:12;
A55: ((GoB f) * (m,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2 by A24, A28, A31, A51, GOBOARD5:1;
( 1 <= i9 & i9 <= len (GoB f) ) by A53, MATRIX_0:32;
then A56: ((GoB f) * (i9,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2 by A31, A51, GOBOARD5:1;
consider i19, j19 being Nat such that
A57: [i19,j19] in Indices G and
A58: f /. l = G * (i19,j19) by A2, A52, GOBOARD1:def 9;
A59: 1 <= j19 by A57, MATRIX_0:32;
A60: ( 1 <= i19 & i19 <= len G ) by A57, MATRIX_0:32;
then A61: (G * (i19,j1)) `2 = (G * (1,j1)) `2 by A8, A12, GOBOARD5:1;

A62: now :: thesis:

assume j1 >= j19 ; :: thesis:
then (G * (i19,j19)) `2 <= (G * (i1,j1)) `2 by A12, A27, A60, A59, A61, SPRECT_3:12;
hence contradiction by A21, A24, A28, A45, A4, A30, A51, A54, A56, A55, A58, GOBOARD5:4; :: thesis:

end;

A63: j19 <= width G by A57, MATRIX_0:32;
A64: (G * (i19,j2)) `2 = (G * (1,j2)) `2 by A16, A11, A60, GOBOARD5:1;

now :: thesis:

assume j2 <= j19 ; :: thesis:
then (G * (i2,j2)) `2 <= (G * (i19,j19)) `2 by A16, A60, A63, A49, A64, SPRECT_3:12;
hence contradiction by A23, A24, A28, A33, A44, A41, A6, A31, A50, A54, A56, A55, A58, GOBOARD5:4; :: thesis:

end;

hence contradiction by A47, A62, NAT_1:13; :: thesis:

end;

now :: thesis:

assume j <= k ; :: thesis:
then A65: ((GoB f) * (i,j)) `2 <= ((GoB f) * (m,k)) `2 by A24, A28, A39, A40, A44, A41, SPRECT_3:12;
j1 < j2 by A47, NAT_1:13;
hence contradiction by A21, A23, A4, A6, A8, A14, A13, A11, A27, A15, A65, GOBOARD5:4; :: thesis:

end;

then k + 1 <= j by NAT_1:13;
then k + 1 = j by A48, XXREAL_0:1;
then A66: ( right_cell (f,n) = cell ((GoB f),m,k) & left_cell (f,n) = cell ((GoB f),(m -' 1),k) ) by A1, A20, A21, A22, A23, A30, A29, GOBOARD5:def 6, GOBOARD5:def 7;
( right_cell (f,n,G) = cell (G,i1,j1) & left_cell (f,n,G) = cell (G,(i1 -' 1),j1) ) by A1, A2, A3, A4, A5, A6, A9, A47, Def1, Def2;
hence ( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) ) by A19, A20, A21, A3, A4, A66, Th10, Th11; :: thesis:

end;

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

A68: now :: thesis:

assume A69: m + 1 < i ; :: thesis:
then A70: m + 1 < len (GoB f) by A36, XXREAL_0:2;
then consider l, j9 being Nat such that
A71: l in dom f and
A72: [(m + 1),j9] in Indices (GoB f) and
A73: f /. l = (GoB f) * ((m + 1),j9) by JORDAN5D:7, NAT_1:12;
A74: ((GoB f) * ((m + 1),k)) `1 = ((GoB f) * ((m + 1),1)) `1 by A45, A39, A38, A70, GOBOARD5:2;
( 1 <= j9 & j9 <= width (GoB f) ) by A72, MATRIX_0:32;
then A75: ((GoB f) * ((m + 1),j9)) `1 = ((GoB f) * ((m + 1),1)) `1 by A38, A70, GOBOARD5:2;
A76: ( 1 <= m + 1 & ((GoB f) * ((m + 1),j)) `1 = ((GoB f) * ((m + 1),1)) `1 ) by A40, A33, A38, A70, GOBOARD5:2;
A77: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A14, A13, A16, A11, GOBOARD5:2;
consider i19, j19 being Nat such that
A78: [i19,j19] in Indices G and
A79: f /. l = G * (i19,j19) by A2, A71, GOBOARD1:def 9;
A80: i19 <= len G by A78, MATRIX_0:32;
A81: ( 1 <= j19 & j19 <= width G ) by A78, MATRIX_0:32;
A82: 1 <= i19 by A78, MATRIX_0:32;
then A83: (G * (i19,j19)) `1 = (G * (i19,1)) `1 by A80, A81, GOBOARD5:2;
A84: (G * (i19,j1)) `1 = (G * (i19,1)) `1 by A8, A12, A82, A80, GOBOARD5:2;

A85: now :: thesis:

assume i1 >= i19 ; :: thesis:
then (G * (i19,j19)) `1 <= (G * (i1,j1)) `1 by A18, A8, A12, A82, A83, A84, SPRECT_3:13;
hence contradiction by A21, A24, A45, A39, A4, A35, A70, A73, A75, A74, A79, GOBOARD5:3; :: thesis:

end;

A86: (G * (i2,j19)) `1 = (G * (i2,1)) `1 by A14, A13, A81, GOBOARD5:2;

now :: thesis:

assume i2 <= i19 ; :: thesis:
then (G * (i2,j2)) `1 <= (G * (i19,j19)) `1 by A14, A80, A81, A77, A86, SPRECT_3:13;
hence contradiction by A23, A36, A40, A33, A6, A69, A73, A75, A76, A79, GOBOARD5:3; :: thesis:

end;

hence contradiction by A67, A85, NAT_1:13; :: thesis:

end;

now :: thesis:

assume i <= m ; :: thesis:
then A87: ((GoB f) * (i,j)) `1 <= ((GoB f) * (m,k)) `1 by A28, A45, A39, A42, A43, A46, SPRECT_3:13;
i1 < i2 by A67, NAT_1:13;
hence contradiction by A21, A23, A4, A6, A25, A8, A12, A13, A67, A87, GOBOARD5:3; :: thesis:

end;

then m + 1 <= i by NAT_1:13;
then m + 1 = i by A68, XXREAL_0:1;
then A88: ( right_cell (f,n) = cell ((GoB f),m,(k -' 1)) & left_cell (f,n) = cell ((GoB f),m,k) ) by A1, A20, A21, A22, A23, A35, A34, GOBOARD5:def 6, GOBOARD5:def 7;
( right_cell (f,n,G) = cell (G,i1,(j1 -' 1)) & left_cell (f,n,G) = cell (G,i1,j1) ) by A1, A2, A3, A4, A5, A6, A10, A67, Def1, Def2;
hence ( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) ) by A19, A20, A21, A3, A4, A88, Th10, Th12; :: thesis:

end;

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

A90: now :: thesis:

assume A91: m > i + 1 ; :: thesis:
then A92: i + 1 < len (GoB f) by A28, XXREAL_0:2;
then consider l, j9 being Nat such that
A93: l in dom f and
A94: [(i + 1),j9] in Indices (GoB f) and
A95: f /. l = (GoB f) * ((i + 1),j9) by JORDAN5D:7, NAT_1:12;
A96: ( 1 <= i + 1 & ((GoB f) * ((i + 1),k)) `1 = ((GoB f) * ((i + 1),1)) `1 ) by A45, A39, A37, A92, GOBOARD5:2;
( 1 <= j9 & j9 <= width (GoB f) ) by A94, MATRIX_0:32;
then A97: ((GoB f) * ((i + 1),j9)) `1 = ((GoB f) * ((i + 1),1)) `1 by A37, A92, GOBOARD5:2;
A98: ((GoB f) * ((i + 1),j)) `1 = ((GoB f) * ((i + 1),1)) `1 by A40, A33, A37, A92, GOBOARD5:2;
A99: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A14, A13, A16, A11, GOBOARD5:2;
consider i19, j19 being Nat such that
A100: [i19,j19] in Indices G and
A101: f /. l = G * (i19,j19) by A2, A93, GOBOARD1:def 9;
A102: 1 <= i19 by A100, MATRIX_0:32;
A103: ( 1 <= j19 & j19 <= width G ) by A100, MATRIX_0:32;
A104: i19 <= len G by A100, MATRIX_0:32;
then A105: (G * (i19,j19)) `1 = (G * (i19,1)) `1 by A102, A103, GOBOARD5:2;
A106: (G * (i19,j1)) `1 = (G * (i19,1)) `1 by A8, A12, A102, A104, GOBOARD5:2;

A107: now :: thesis:

assume i1 <= i19 ; :: thesis:
then (G * (i19,j19)) `1 >= (G * (i1,j1)) `1 by A25, A8, A12, A104, A105, A106, SPRECT_3:13;
hence contradiction by A21, A28, A45, A39, A4, A91, A95, A97, A96, A101, GOBOARD5:3; :: thesis:

end;

A108: (G * (i2,j19)) `1 = (G * (i2,1)) `1 by A14, A13, A103, GOBOARD5:2;

now :: thesis:

assume i2 >= i19 ; :: thesis:
then (G * (i2,j2)) `1 >= (G * (i19,j19)) `1 by A13, A102, A103, A99, A108, SPRECT_3:13;
hence contradiction by A23, A42, A40, A33, A6, A34, A92, A95, A97, A98, A101, GOBOARD5:3; :: thesis:

end;

hence contradiction by A89, A107, NAT_1:13; :: thesis:

end;

now :: thesis:

assume m <= i ; :: thesis:
then A109: ((GoB f) * (i,j)) `1 >= ((GoB f) * (m,k)) `1 by A24, A45, A39, A36, A43, A46, SPRECT_3:13;
i1 > i2 by A89, NAT_1:13;
hence contradiction by A21, A23, A4, A6, A18, A8, A12, A14, A89, A109, GOBOARD5:3; :: thesis:

end;

then i + 1 <= m by NAT_1:13;
then i + 1 = m by A90, XXREAL_0:1;
then A110: ( right_cell (f,n) = cell ((GoB f),i,j) & left_cell (f,n) = cell ((GoB f),i,(j -' 1)) ) by A1, A20, A21, A22, A23, A35, A34, GOBOARD5:def 6, GOBOARD5:def 7;
( right_cell (f,n,G) = cell (G,i2,j2) & left_cell (f,n,G) = cell (G,i2,(j2 -' 1)) ) by A1, A2, A3, A4, A5, A6, A10, A89, Def1, Def2;
hence ( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) ) by A19, A22, A23, A5, A6, A110, Th10, Th12; :: thesis:

end;

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

A112: now :: thesis:

A113: (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A14, A13, A16, A11, GOBOARD5:1;
assume A114: j + 1 < k ; :: thesis:
then A115: j + 1 < width (GoB f) by A39, XXREAL_0:2;
then consider l, i9 being Nat such that
A116: l in dom f and
A117: [i9,(j + 1)] in Indices (GoB f) and
A118: f /. l = (GoB f) * (i9,(j + 1)) by JORDAN5D:8, NAT_1:12;
A119: ((GoB f) * (m,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A24, A28, A32, A115, GOBOARD5:1;
( 1 <= i9 & i9 <= len (GoB f) ) by A117, MATRIX_0:32;
then A120: ((GoB f) * (i9,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A32, A115, GOBOARD5:1;
consider i19, j19 being Nat such that
A121: [i19,j19] in Indices G and
A122: f /. l = G * (i19,j19) by A2, A116, GOBOARD1:def 9;
A123: j19 <= width G by A121, MATRIX_0:32;
A124: ( 1 <= i19 & i19 <= len G ) by A121, MATRIX_0:32;
then A125: (G * (i19,j1)) `2 = (G * (1,j1)) `2 by A8, A12, GOBOARD5:1;

A126: now :: thesis:

assume j1 <= j19 ; :: thesis:
then (G * (i19,j19)) `2 >= (G * (i1,j1)) `2 by A8, A27, A124, A123, A125, SPRECT_3:12;
hence contradiction by A21, A24, A28, A39, A4, A32, A114, A118, A120, A119, A122, GOBOARD5:4; :: thesis:

end;

A127: ((GoB f) * (i,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A42, A36, A32, A115, GOBOARD5:1;
A128: 1 <= j19 by A121, MATRIX_0:32;
A129: (G * (i19,j2)) `2 = (G * (1,j2)) `2 by A16, A11, A124, GOBOARD5:1;

now :: thesis:

assume j2 >= j19 ; :: thesis:
then (G * (i2,j2)) `2 >= (G * (i19,j19)) `2 by A11, A124, A128, A113, A129, SPRECT_3:12;
hence contradiction by A23, A42, A36, A40, A6, A29, A115, A118, A120, A127, A122, GOBOARD5:4; :: thesis:

end;

hence contradiction by A111, A126, NAT_1:13; :: thesis:

end;

now :: thesis:

assume j >= k ; :: thesis:
then A130: ((GoB f) * (i,j)) `2 >= ((GoB f) * (m,k)) `2 by A24, A28, A45, A33, A44, A41, SPRECT_3:12;
j1 > j2 by A111, NAT_1:13;
hence contradiction by A21, A23, A4, A6, A12, A14, A13, A16, A27, A15, A130, GOBOARD5:4; :: thesis:

end;

then j + 1 <= k by NAT_1:13;
then j + 1 = k by A112, XXREAL_0:1;
then A131: ( right_cell (f,n) = cell ((GoB f),(m -' 1),j) & left_cell (f,n) = cell ((GoB f),m,j) ) by A1, A20, A21, A22, A23, A30, A29, GOBOARD5:def 6, GOBOARD5:def 7;

A132: now :: thesis:

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

per cases by A133, XXREAL_0:1;

suppose m < i ; :: thesis:

hence contradiction by A21, A23, A24, A45, A39, A36, A43, A46, A4, A6, A26, A17, A111, GOBOARD5:3; :: thesis:

end;

suppose m > i ; :: thesis:

hence contradiction by A21, A23, A28, A45, A39, A42, A43, A46, A4, A6, A26, A17, A111, GOBOARD5:3; :: thesis:

end;

( right_cell (f,n,G) = cell (G,(i1 -' 1),j2) & left_cell (f,n,G) = cell (G,i1,j2) ) by A1, A2, A3, A4, A5, A6, A9, A111, Def1, Def2;
hence ( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) ) by A19, A22, A23, A5, A6, A111, A132, A131, Th10, Th11; :: thesis:

end;