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 <= width (GoB f) ) and
A3: LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) c= L~ f and
A4: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) c= L~ f ; :: thesis:
A5: 1 <= i + 1 by NAT_1:11;
A6: i + (1 + 1) = (i + 1) + 1 ;
then A7: i + 2 <= len (GoB f) by A1, NAT_1:13;
A8: 1 <= i + 2 by A6, NAT_1:11;
A9: i < len (GoB f) by A1, NAT_1:13;
(1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),j)) in LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) by RLTOPSP1:70;
then consider k1 being Element of NAT such that
A10: ( 1 <= k1 & k1 + 1 <= len f ) and
A11: LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k1 by A1, A2, A3, Th42;
A12: k1 < len f by A10, NAT_1:13;
(1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 2),j)) in LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) by RLTOPSP1:70;
then consider k2 being Element of NAT such that
A13: ( 1 <= k2 & k2 + 1 <= len f ) and
A14: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) = LSeg f,k2 by A2, A4, A5, A6, A7, Th42;
A15: k2 < len f by A13, NAT_1:13;

A16: 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;

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

A18: ( ( k1 = 1 or k1 > 1 ) & ( k2 = 1 or k2 > 1 ) ) by A10, A13, XXREAL_0:1;

now

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

case k1 = k2 ; :: thesis:

then A55: ( (GoB f) * i,j = (GoB f) * (i + 2),j or (GoB f) * i,j = (GoB f) * (i + 1),j ) by A11, A14, SPPOL_1:25;
( [i,j] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & [(i + 2),j] in Indices (GoB f) ) by A1, A2, A5, A7, A8, A9, MATRIX_1:37;
then ( i = i + 1 or i = i + 2 ) by A55, GOBOARD1:21;
hence contradiction ; :: thesis:

end;

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

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

end;

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

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

end;

hence ( ( f /. 1 = (GoB f) * (i + 1),j & ( ( f /. 2 = (GoB f) * i,j & f /. ((len f) -' 1) = (GoB f) * (i + 2),j ) or ( f /. 2 = (GoB f) * (i + 2),j & 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 + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 2),j ) or ( f /. k = (GoB f) * (i + 2),j & f /. (k + 2) = (GoB f) * i,j ) ) ) ) ; :: thesis: