let i, j be Element of NAT ; :: thesis:
let f be non constant standard special_circular_sequence; :: thesis:
assume that
A1: 1 <= i and
A2: i + 1 <= len (GoB f) and
A3: 1 <= j and
A4: j + 1 <= width (GoB f) and
A5: LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) c= L~ f and
A6: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) c= L~ f ; :: thesis:
A7: j < width (GoB f) by A4, NAT_1:13;
A8: i < len (GoB f) by A2, NAT_1:13;
A9: 1 <= j + 1 by NAT_1:11;
(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 and
A11: k1 + 1 <= len f and
A12: LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k1 by A1, A2, A3, A5, A7, Th42;
A13: k1 < len f by A11, NAT_1:13;

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

A15: 1 <= i + 1 by NAT_1:11;
(1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 1),(j + 1))) in LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) by RLTOPSP1:70;
then consider k2 being Element of NAT such that
A16: 1 <= k2 and
A17: k2 + 1 <= len f and
A18: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) = LSeg f,k2 by A2, A3, A4, A6, A15, Th41;
A19: k2 < len f by A17, NAT_1:13;

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

A21: ( k1 = 1 or k1 > 1 ) by A10, XXREAL_0:1;

now

per cases by A16, A14, A20, A21, XXREAL_0:1;

case that A22: k1 = 1 and
A23: k2 = 2 ; :: thesis:

A24: LSeg f,2 = LSeg (f /. 2),(f /. (2 + 1)) by A17, A23, TOPREAL1:def 5;
then A25: ( ( (GoB f) * (i + 1),j = f /. 2 & (GoB f) * (i + 1),(j + 1) = f /. (2 + 1) ) or ( (GoB f) * (i + 1),j = f /. (2 + 1) & (GoB f) * (i + 1),(j + 1) = f /. 2 ) ) by A18, A23, SPPOL_1:25;
thus ( 1 <= 1 & 1 + 1 < len f ) by A17, A23, NAT_1:13; :: thesis:
A26: 3 < len f by Th36, XXREAL_0:2;
then A27: f /. 1 <> f /. 3 by Th38;
A28: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A11, A22, TOPREAL1:def 5;
then A29: ( ( (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 A12, A22, SPPOL_1:25;
hence f /. (1 + 1) = (GoB f) * (i + 1),j by A25, A26, Th38; :: thesis:
thus f /. 1 = (GoB f) * i,j by A18, A23, A29, A24, A27, SPPOL_1:25; :: thesis:
thus f /. (1 + 2) = (GoB f) * (i + 1),(j + 1) by A12, A22, A28, A25, A27, SPPOL_1:25; :: thesis:

end;

case that A30: k1 = 1 and
A31: k2 > 2 ; :: thesis:

A32: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A11, A30, TOPREAL1:def 5;
then A33: ( ( (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 A12, A30, SPPOL_1:25;
A34: 2 < k2 + 1 by A31, NAT_1:13;
then A35: f /. (k2 + 1) <> f /. 2 by A17, Th39;
LSeg f,k2 = LSeg (f /. k2),(f /. (k2 + 1)) by A16, A17, TOPREAL1:def 5;
then A36: ( ( (GoB f) * (i + 1),j = f /. k2 & (GoB f) * (i + 1),(j + 1) = f /. (k2 + 1) ) or ( (GoB f) * (i + 1),j = f /. (k2 + 1) & (GoB f) * (i + 1),(j + 1) = f /. k2 ) ) by A18, SPPOL_1:25;
A37: f /. k2 <> f /. 2 by A19, A31, Th38;
hence f /. 1 = (GoB f) * (i + 1),j by A12, A30, A32, A36, A35, SPPOL_1:25; :: thesis:
thus f /. 2 = (GoB f) * i,j by A12, A30, A32, A36, A37, A35, SPPOL_1:25; :: thesis:
A38: k2 > 1 by A31, XXREAL_0:2;
then A39: k2 + 1 > 1 by NAT_1:13;
then k2 + 1 = len f by A17, A19, A31, A33, A36, A38, A34, Th39, Th40;
then k2 + 1 = ((len f) -' 1) + 1 by A39, XREAL_1:237;
hence f /. ((len f) -' 1) = (GoB f) * (i + 1),(j + 1) by A19, A31, A33, A36, A38, Th38; :: thesis:

end;

case that A40: k2 = 1 and
A41: k1 = 2 ; :: thesis:

A42: LSeg f,2 = LSeg (f /. 2),(f /. (2 + 1)) by A11, A41, TOPREAL1:def 5;
then A43: ( ( (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 A12, A41, SPPOL_1:25;
thus ( 1 <= 1 & 1 + 1 < len f ) by A11, A41, NAT_1:13; :: thesis:
A44: 3 < len f by Th36, XXREAL_0:2;
then A45: f /. 1 <> f /. 3 by Th38;
A46: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A17, A40, TOPREAL1:def 5;
then A47: ( ( (GoB f) * (i + 1),(j + 1) = f /. 1 & (GoB f) * (i + 1),j = f /. 2 ) or ( (GoB f) * (i + 1),(j + 1) = f /. 2 & (GoB f) * (i + 1),j = f /. 1 ) ) by A18, A40, SPPOL_1:25;
hence f /. (1 + 1) = (GoB f) * (i + 1),j by A43, A44, Th38; :: thesis:
thus f /. 1 = (GoB f) * (i + 1),(j + 1) by A12, A41, A47, A42, A45, SPPOL_1:25; :: thesis:
thus f /. (1 + 2) = (GoB f) * i,j by A18, A40, A46, A43, A45, SPPOL_1:25; :: thesis:

end;

case that A48: k2 = 1 and
A49: k1 > 2 ; :: thesis:

A50: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A17, A48, TOPREAL1:def 5;
then A51: ( ( (GoB f) * (i + 1),(j + 1) = f /. 1 & (GoB f) * (i + 1),j = f /. 2 ) or ( (GoB f) * (i + 1),(j + 1) = f /. 2 & (GoB f) * (i + 1),j = f /. 1 ) ) by A18, A48, SPPOL_1:25;
A52: 2 < k1 + 1 by A49, NAT_1:13;
then A53: f /. (k1 + 1) <> f /. 2 by A11, Th39;
LSeg f,k1 = LSeg (f /. k1),(f /. (k1 + 1)) by A10, A11, TOPREAL1:def 5;
then A54: ( ( (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 A12, SPPOL_1:25;
A55: f /. k1 <> f /. 2 by A13, A49, Th38;
hence f /. 1 = (GoB f) * (i + 1),j by A18, A48, A50, A54, A53, SPPOL_1:25; :: thesis:
thus f /. 2 = (GoB f) * (i + 1),(j + 1) by A18, A48, A50, A54, A55, A53, SPPOL_1:25; :: thesis:
A56: k1 > 1 by A49, XXREAL_0:2;
then A57: k1 + 1 > 1 by NAT_1:13;
then k1 + 1 = len f by A11, A13, A49, A51, A54, A56, A52, Th39, Th40;
then k1 + 1 = ((len f) -' 1) + 1 by A57, XREAL_1:237;
hence f /. ((len f) -' 1) = (GoB f) * i,j by A13, A49, A51, A54, A56, Th38; :: thesis:

end;

case k1 = k2 ; :: thesis:

then A58: ( (GoB f) * i,j = (GoB f) * (i + 1),(j + 1) or (GoB f) * i,j = (GoB f) * (i + 1),j ) by A12, A18, SPPOL_1:25;
A59: [(i + 1),(j + 1)] in Indices (GoB f) by A2, A4, A15, A9, MATRIX_1:37;
( [i,j] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) ) by A1, A2, A3, A15, A8, A7, MATRIX_1:37;
then i = i + 1 by A58, A59, GOBOARD1:21;
hence contradiction ; :: thesis:

end;

case that A60: k1 > 1 and
A61: k2 > k1 ; :: thesis:

A62: ( 1 < k1 + 1 & k1 + 1 < k2 + 1 ) by A60, A61, NAT_1:13, XREAL_1:8;
A63: k1 < k2 + 1 by A61, NAT_1:13;
then A64: f /. k1 <> f /. (k2 + 1) by A17, A60, Th39;
A65: k1 + 1 <= k2 by A61, NAT_1:13;
LSeg f,k2 = LSeg (f /. k2),(f /. (k2 + 1)) by A16, A17, TOPREAL1:def 5;
then A66: ( ( (GoB f) * (i + 1),j = f /. k2 & (GoB f) * (i + 1),(j + 1) = f /. (k2 + 1) ) or ( (GoB f) * (i + 1),j = f /. (k2 + 1) & (GoB f) * (i + 1),(j + 1) = f /. k2 ) ) by A18, SPPOL_1:25;
A67: k2 < len f by A17, NAT_1:13;
then A68: f /. k1 <> f /. k2 by A60, A61, Th39;
A69: LSeg f,k1 = LSeg (f /. k1),(f /. (k1 + 1)) by A10, A11, TOPREAL1:def 5;
then ( ( (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 A12, SPPOL_1:25;
then k1 + 1 >= k2 by A17, A60, A61, A66, A63, A67, A62, Th39;
then A70: k1 + 1 = k2 by A65, XXREAL_0:1;
hence ( 1 <= k1 & k1 + 1 < len f ) by A17, A60, NAT_1:13; :: thesis:
thus f /. (k1 + 1) = (GoB f) * (i + 1),j by A12, A69, A66, A64, A68, SPPOL_1:25; :: thesis:
thus f /. k1 = (GoB f) * i,j by A12, A69, A66, A64, A68, SPPOL_1:25; :: thesis:
thus f /. (k1 + 2) = (GoB f) * (i + 1),(j + 1) by A12, A69, A66, A64, A70, SPPOL_1:25; :: thesis:

end;

case that A71: k2 > 1 and
A72: k1 > k2 ; :: thesis:

A73: ( 1 < k2 + 1 & k2 + 1 < k1 + 1 ) by A71, A72, NAT_1:13, XREAL_1:8;
A74: k2 < k1 + 1 by A72, NAT_1:13;
then A75: f /. k2 <> f /. (k1 + 1) by A11, A71, Th39;
A76: k2 + 1 <= k1 by A72, NAT_1:13;
LSeg f,k1 = LSeg (f /. k1),(f /. (k1 + 1)) by A10, A11, TOPREAL1:def 5;
then A77: ( ( (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 A12, SPPOL_1:25;
A78: k1 < len f by A11, NAT_1:13;
then A79: f /. k2 <> f /. k1 by A71, A72, Th39;
A80: LSeg f,k2 = LSeg (f /. k2),(f /. (k2 + 1)) by A16, A17, TOPREAL1:def 5;
then ( ( (GoB f) * (i + 1),(j + 1) = f /. k2 & (GoB f) * (i + 1),j = f /. (k2 + 1) ) or ( (GoB f) * (i + 1),(j + 1) = f /. (k2 + 1) & (GoB f) * (i + 1),j = f /. k2 ) ) by A18, SPPOL_1:25;
then k2 + 1 >= k1 by A11, A71, A72, A77, A74, A78, A73, Th39;
then A81: k2 + 1 = k1 by A76, XXREAL_0:1;
hence ( 1 <= k2 & k2 + 1 < len f ) by A11, A71, NAT_1:13; :: thesis:
thus f /. (k2 + 1) = (GoB f) * (i + 1),j by A18, A80, A77, A75, A79, SPPOL_1:25; :: thesis:
thus f /. k2 = (GoB f) * (i + 1),(j + 1) by A18, A80, A77, A75, A79, SPPOL_1:25; :: thesis:
thus f /. (k2 + 2) = (GoB f) * i,j by A18, A80, A77, A75, A81, 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 + 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 + 1),j & ( ( 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: