let i, j be Element of NAT ; :: thesis:
let f be non constant standard special_circular_sequence; :: thesis:
assume that
A1: ( 1 <= i & i + 1 <= len (GoB f) ) and
A2: ( 1 <= j & j + 1 <= width (GoB f) ) and
A3: LSeg ((GoB f) * i,j),((GoB f) * i,(j + 1)) c= L~ f and
A4: LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) c= L~ f ; :: thesis:
A5: 1 <= j + 1 by NAT_1:11;
A6: j < width (GoB f) by A2, NAT_1:13;
A7: 1 <= i + 1 by NAT_1:11;
A8: i < len (GoB f) by A1, NAT_1:13;
(1 / 2) * (((GoB f) * i,j) + ((GoB f) * i,(j + 1))) in LSeg ((GoB f) * i,j),((GoB f) * i,(j + 1)) by RLTOPSP1:70;
then consider k1 being Element of NAT such that
A9: ( 1 <= k1 & k1 + 1 <= len f ) and
A10: LSeg ((GoB f) * i,j),((GoB f) * i,(j + 1)) = LSeg f,k1 by A1, A2, A3, A8, Th41;
A11: k1 < len f by A9, NAT_1:13;
(1 / 2) * (((GoB f) * i,(j + 1)) + ((GoB f) * (i + 1),(j + 1))) in LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) by RLTOPSP1:70;
then consider k2 being Element of NAT such that
A12: ( 1 <= k2 & k2 + 1 <= len f ) and
A13: LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) = LSeg f,k2 by A1, A2, A4, A5, Th42;
A14: k2 < len f by A12, NAT_1:13;

A15: now

assume k1 > 1 ; :: thesis:
then k1 >= 1 + 1 by NAT_1:13;
hence ( k1 = 2 or k1 > 2 ) by XXREAL_0:1; :: thesis:

end;

A16: now

assume k2 > 1 ; :: thesis:
then k2 >= 1 + 1 by NAT_1:13;
hence ( k2 = 2 or k2 > 2 ) by XXREAL_0:1; :: thesis:

end;

A17: ( ( k1 = 1 or k1 > 1 ) & ( k2 = 1 or k2 > 1 ) ) by A9, A12, XXREAL_0:1;

now

per cases by A15, A16, A17, XXREAL_0:1;

case that A18: k1 = 1 and
A19: k2 = 2 ; :: thesis:

A20: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A9, A18, TOPREAL1:def 5;
then A21: ( ( (GoB f) * i,j = f /. 1 & (GoB f) * i,(j + 1) = f /. 2 ) or ( (GoB f) * i,j = f /. 2 & (GoB f) * i,(j + 1) = f /. 1 ) ) by A10, A18, SPPOL_1:25;
A22: LSeg f,2 = LSeg (f /. 2),(f /. (2 + 1)) by A12, A19, TOPREAL1:def 5;
then A23: ( ( (GoB f) * i,(j + 1) = f /. 2 & (GoB f) * (i + 1),(j + 1) = f /. (2 + 1) ) or ( (GoB f) * i,(j + 1) = f /. (2 + 1) & (GoB f) * (i + 1),(j + 1) = f /. 2 ) ) by A13, A19, SPPOL_1:25;
thus ( 1 <= 1 & 1 + 1 < len f ) by A12, A19, NAT_1:13; :: thesis:
A24: 3 < len f by Th36, XXREAL_0:2;
then A25: f /. 1 <> f /. 3 by Th38;
thus f /. (1 + 1) = (GoB f) * i,(j + 1) by A21, A23, A24, Th38; :: thesis:
thus f /. 1 = (GoB f) * i,j by A13, A19, A21, A22, A25, SPPOL_1:25; :: thesis:
thus f /. (1 + 2) = (GoB f) * (i + 1),(j + 1) by A10, A18, A20, A23, A25, SPPOL_1:25; :: thesis:

end;

case that A26: k1 = 1 and
A27: k2 > 2 ; :: thesis:

A28: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A9, A26, TOPREAL1:def 5;
then A29: ( ( (GoB f) * i,j = f /. 1 & (GoB f) * i,(j + 1) = f /. 2 ) or ( (GoB f) * i,j = f /. 2 & (GoB f) * i,(j + 1) = f /. 1 ) ) by A10, A26, SPPOL_1:25;
LSeg f,k2 = LSeg (f /. k2),(f /. (k2 + 1)) by A12, TOPREAL1:def 5;
then A30: ( ( (GoB f) * i,(j + 1) = f /. k2 & (GoB f) * (i + 1),(j + 1) = f /. (k2 + 1) ) or ( (GoB f) * i,(j + 1) = f /. (k2 + 1) & (GoB f) * (i + 1),(j + 1) = f /. k2 ) ) by A13, SPPOL_1:25;
A31: f /. k2 <> f /. 2 by A14, A27, Th38;
A32: k2 > 1 by A27, XXREAL_0:2;
A33: 2 < k2 + 1 by A27, NAT_1:13;
then A34: f /. (k2 + 1) <> f /. 2 by A12, Th39;
hence f /. 1 = (GoB f) * i,(j + 1) by A10, A26, A28, A30, A31, SPPOL_1:25; :: thesis:
thus f /. 2 = (GoB f) * i,j by A10, A26, A28, A30, A31, A34, SPPOL_1:25; :: thesis:
A35: k2 + 1 > 1 by A32, NAT_1:13;
then k2 + 1 = len f by A12, A14, A27, A29, A30, A32, A33, Th39, Th40;
then k2 + 1 = ((len f) -' 1) + 1 by A35, XREAL_1:237;
hence f /. ((len f) -' 1) = (GoB f) * (i + 1),(j + 1) by A14, A27, A29, A30, A32, Th38; :: thesis:

end;

case that A36: k2 = 1 and
A37: k1 = 2 ; :: thesis:

A38: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A12, A36, TOPREAL1:def 5;
then A39: ( ( (GoB f) * (i + 1),(j + 1) = f /. 1 & (GoB f) * i,(j + 1) = f /. 2 ) or ( (GoB f) * (i + 1),(j + 1) = f /. 2 & (GoB f) * i,(j + 1) = f /. 1 ) ) by A13, A36, SPPOL_1:25;
A40: LSeg f,2 = LSeg (f /. 2),(f /. (2 + 1)) by A9, A37, TOPREAL1:def 5;
then A41: ( ( (GoB f) * i,(j + 1) = f /. 2 & (GoB f) * i,j = f /. (2 + 1) ) or ( (GoB f) * i,(j + 1) = f /. (2 + 1) & (GoB f) * i,j = f /. 2 ) ) by A10, A37, SPPOL_1:25;
thus ( 1 <= 1 & 1 + 1 < len f ) by A9, A37, NAT_1:13; :: thesis:
A42: 3 < len f by Th36, XXREAL_0:2;
then A43: f /. 1 <> f /. 3 by Th38;
thus f /. (1 + 1) = (GoB f) * i,(j + 1) by A39, A41, A42, Th38; :: thesis:
thus f /. 1 = (GoB f) * (i + 1),(j + 1) by A10, A37, A39, A40, A43, SPPOL_1:25; :: thesis:
thus f /. (1 + 2) = (GoB f) * i,j by A13, A36, A38, A41, A43, SPPOL_1:25; :: thesis:

end;

case that A44: k2 = 1 and
A45: k1 > 2 ; :: thesis:

A46: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A12, A44, TOPREAL1:def 5;
then A47: ( ( (GoB f) * (i + 1),(j + 1) = f /. 1 & (GoB f) * i,(j + 1) = f /. 2 ) or ( (GoB f) * (i + 1),(j + 1) = f /. 2 & (GoB f) * i,(j + 1) = f /. 1 ) ) by A13, A44, SPPOL_1:25;
LSeg f,k1 = LSeg (f /. k1),(f /. (k1 + 1)) by A9, TOPREAL1:def 5;
then A48: ( ( (GoB f) * i,(j + 1) = f /. k1 & (GoB f) * i,j = f /. (k1 + 1) ) or ( (GoB f) * i,(j + 1) = f /. (k1 + 1) & (GoB f) * i,j = f /. k1 ) ) by A10, SPPOL_1:25;
A49: f /. k1 <> f /. 2 by A11, A45, Th38;
A50: k1 > 1 by A45, XXREAL_0:2;
A51: 2 < k1 + 1 by A45, NAT_1:13;
then A52: f /. (k1 + 1) <> f /. 2 by A9, Th39;
hence f /. 1 = (GoB f) * i,(j + 1) by A13, A44, A46, A48, A49, SPPOL_1:25; :: thesis:
thus f /. 2 = (GoB f) * (i + 1),(j + 1) by A13, A44, A46, A48, A49, A52, SPPOL_1:25; :: thesis:
A53: k1 + 1 > 1 by A50, NAT_1:13;
then k1 + 1 = len f by A9, A11, A45, A47, A48, A50, A51, Th39, Th40;
then k1 + 1 = ((len f) -' 1) + 1 by A53, XREAL_1:237;
hence f /. ((len f) -' 1) = (GoB f) * i,j by A11, A45, A47, A48, A50, Th38; :: thesis:

end;

case k1 = k2 ; :: thesis:

then A54: ( (GoB f) * i,j = (GoB f) * (i + 1),(j + 1) or (GoB f) * i,j = (GoB f) * i,(j + 1) ) by A10, A13, SPPOL_1:25;
( [i,j] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A5, A6, A7, A8, MATRIX_1:37;
then j = j + 1 by A54, GOBOARD1:21;
hence contradiction ; :: thesis:

end;

case that A55: k1 > 1 and
A56: k2 > k1 ; :: thesis:

A57: LSeg f,k1 = LSeg (f /. k1),(f /. (k1 + 1)) by A9, TOPREAL1:def 5;
then A58: ( ( (GoB f) * i,j = f /. k1 & (GoB f) * i,(j + 1) = f /. (k1 + 1) ) or ( (GoB f) * i,j = f /. (k1 + 1) & (GoB f) * i,(j + 1) = f /. k1 ) ) by A10, SPPOL_1:25;
LSeg f,k2 = LSeg (f /. k2),(f /. (k2 + 1)) by A12, TOPREAL1:def 5;
then A59: ( ( (GoB f) * i,(j + 1) = f /. k2 & (GoB f) * (i + 1),(j + 1) = f /. (k2 + 1) ) or ( (GoB f) * i,(j + 1) = f /. (k2 + 1) & (GoB f) * (i + 1),(j + 1) = f /. k2 ) ) by A13, SPPOL_1:25;
A60: k1 < k2 + 1 by A56, NAT_1:13;
then A61: f /. k1 <> f /. (k2 + 1) by A12, A55, Th39;
A62: k2 < len f by A12, NAT_1:13;
then A63: f /. k1 <> f /. k2 by A55, A56, Th39;
A64: 1 < k1 + 1 by A55, NAT_1:13;
k1 + 1 < k2 + 1 by A56, XREAL_1:8;
then A65: k1 + 1 >= k2 by A12, A55, A56, A58, A59, A60, A62, A64, Th39;
k1 + 1 <= k2 by A56, NAT_1:13;
then A66: k1 + 1 = k2 by A65, XXREAL_0:1;
hence ( 1 <= k1 & k1 + 1 < len f ) by A12, A55, NAT_1:13; :: thesis:
thus f /. (k1 + 1) = (GoB f) * i,(j + 1) by A10, A57, A59, A61, A63, SPPOL_1:25; :: thesis:
thus f /. k1 = (GoB f) * i,j by A10, A57, A59, A61, A63, SPPOL_1:25; :: thesis:
thus f /. (k1 + 2) = (GoB f) * (i + 1),(j + 1) by A10, A57, A59, A61, A66, SPPOL_1:25; :: thesis:

end;

case that A67: k2 > 1 and
A68: k1 > k2 ; :: thesis:

A69: LSeg f,k2 = LSeg (f /. k2),(f /. (k2 + 1)) by A12, TOPREAL1:def 5;
then A70: ( ( (GoB f) * (i + 1),(j + 1) = f /. k2 & (GoB f) * i,(j + 1) = f /. (k2 + 1) ) or ( (GoB f) * (i + 1),(j + 1) = f /. (k2 + 1) & (GoB f) * i,(j + 1) = f /. k2 ) ) by A13, SPPOL_1:25;
LSeg f,k1 = LSeg (f /. k1),(f /. (k1 + 1)) by A9, TOPREAL1:def 5;
then A71: ( ( (GoB f) * i,(j + 1) = f /. k1 & (GoB f) * i,j = f /. (k1 + 1) ) or ( (GoB f) * i,(j + 1) = f /. (k1 + 1) & (GoB f) * i,j = f /. k1 ) ) by A10, SPPOL_1:25;
A72: k2 < k1 + 1 by A68, NAT_1:13;
then A73: f /. k2 <> f /. (k1 + 1) by A9, A67, Th39;
A74: k1 < len f by A9, NAT_1:13;
then A75: f /. k2 <> f /. k1 by A67, A68, Th39;
A76: 1 < k2 + 1 by A67, NAT_1:13;
k2 + 1 < k1 + 1 by A68, XREAL_1:8;
then A77: k2 + 1 >= k1 by A9, A67, A68, A70, A71, A72, A74, A76, Th39;
k2 + 1 <= k1 by A68, NAT_1:13;
then A78: k2 + 1 = k1 by A77, XXREAL_0:1;
hence ( 1 <= k2 & k2 + 1 < len f ) by A9, A67, NAT_1:13; :: thesis:
thus f /. (k2 + 1) = (GoB f) * i,(j + 1) by A13, A69, A71, A73, A75, SPPOL_1:25; :: thesis:
thus f /. k2 = (GoB f) * (i + 1),(j + 1) by A13, A69, A71, A73, A75, SPPOL_1:25; :: thesis:
thus f /. (k2 + 2) = (GoB f) * i,j by A13, A69, A71, A73, A78, SPPOL_1:25; :: thesis:

end;

hence ( ( f /. 1 = (GoB f) * i,(j + 1) & ( ( f /. 2 = (GoB f) * i,j & f /. ((len f) -' 1) = (GoB f) * (i + 1),(j + 1) ) or ( f /. 2 = (GoB f) * (i + 1),(j + 1) & f /. ((len f) -' 1) = (GoB f) * i,j ) ) ) or ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * i,(j + 1) & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 2) = (GoB f) * i,j ) ) ) ) ; :: thesis: