let i, j be Nat; :: thesis:
let f be V8() 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 + 1),j)),((GoB f) * ((i + 1),(j + 1)))) c= L~ f and
A6: LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * (i,(j + 1)))) c= L~ f ; :: thesis:
A7: 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:69;
then consider k1 being Nat such that
A8: 1 <= k1 and
A9: k1 + 1 <= len f and
A10: LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k1) by A2, A3, A4, A5, A7, Th39;
A11: k1 < len f by A9, NAT_1:13;

A12: now :: thesis:

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

end;

A13: ( i < len (GoB f) & j < width (GoB f) ) by A2, A4, NAT_1:13;
A14: 1 <= j + 1 by NAT_1:11;
(1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 1)))) in LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * (i,(j + 1)))) by RLTOPSP1:69;
then consider k2 being Nat such that
A15: 1 <= k2 and
A16: k2 + 1 <= len f and
A17: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k2) by A1, A2, A4, A6, A14, Th40;
A18: k2 < len f by A16, NAT_1:13;

A19: now :: thesis:

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

end;

A20: ( k1 = 1 or k1 > 1 ) by A8, XXREAL_0:1;

now :: thesis:

per cases by A15, A12, A19, A20, XXREAL_0:1;

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

A23: LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1))) by A16, A22, TOPREAL1:def 3;
then A24: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. (2 + 1) ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. (2 + 1) & (GoB f) * (i,(j + 1)) = f /. 2 ) ) by A17, A22, SPPOL_1:8;
thus ( 1 <= 1 & 1 + 1 < len f ) by A16, A22, NAT_1:13; :: thesis:
A25: 3 < len f by Th34, XXREAL_0:2;
then A26: f /. 1 <> f /. 3 by Th36;
A27: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A9, A21, TOPREAL1:def 3;
then A28: ( ( (GoB f) * ((i + 1),j) = f /. 1 & (GoB f) * ((i + 1),(j + 1)) = f /. 2 ) or ( (GoB f) * ((i + 1),j) = f /. 2 & (GoB f) * ((i + 1),(j + 1)) = f /. 1 ) ) by A10, A21, SPPOL_1:8;
hence f /. (1 + 1) = (GoB f) * ((i + 1),(j + 1)) by A24, A25, Th36; :: thesis:
thus f /. 1 = (GoB f) * ((i + 1),j) by A17, A22, A28, A23, A26, SPPOL_1:8; :: thesis:
thus f /. (1 + 2) = (GoB f) * (i,(j + 1)) by A10, A21, A27, A24, A26, SPPOL_1:8; :: thesis:

end;

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

A31: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A9, A29, TOPREAL1:def 3;
then A32: ( ( (GoB f) * ((i + 1),j) = f /. 1 & (GoB f) * ((i + 1),(j + 1)) = f /. 2 ) or ( (GoB f) * ((i + 1),j) = f /. 2 & (GoB f) * ((i + 1),(j + 1)) = f /. 1 ) ) by A10, A29, SPPOL_1:8;
A33: 2 < k2 + 1 by A30, NAT_1:13;
then A34: f /. (k2 + 1) <> f /. 2 by A16, Th37;
LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by A15, A16, TOPREAL1:def 3;
then A35: ( ( (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 A17, SPPOL_1:8;
A36: f /. k2 <> f /. 2 by A18, A30, Th36;
hence f /. 1 = (GoB f) * ((i + 1),(j + 1)) by A10, A29, A31, A35, A34, SPPOL_1:8; :: thesis:
thus f /. 2 = (GoB f) * ((i + 1),j) by A10, A29, A31, A35, A36, A34, SPPOL_1:8; :: thesis:
A37: k2 > 1 by A30, XXREAL_0:2;
then A38: k2 + 1 > 1 by NAT_1:13;
then k2 + 1 = len f by A16, A18, A30, A32, A35, A37, A33, Th37, Th38;
then k2 + 1 = ((len f) -' 1) + 1 by A38, XREAL_1:235;
hence f /. ((len f) -' 1) = (GoB f) * (i,(j + 1)) by A18, A30, A32, A35, A37, Th36; :: thesis:

end;

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

A41: LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1))) by A9, A40, TOPREAL1:def 3;
then A42: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. 2 & (GoB f) * ((i + 1),j) = f /. (2 + 1) ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. (2 + 1) & (GoB f) * ((i + 1),j) = f /. 2 ) ) by A10, A40, SPPOL_1:8;
thus ( 1 <= 1 & 1 + 1 < len f ) by A9, A40, NAT_1:13; :: thesis:
A43: 3 < len f by Th34, XXREAL_0:2;
then A44: f /. 1 <> f /. 3 by Th36;
A45: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A16, A39, TOPREAL1:def 3;
then A46: ( ( (GoB f) * (i,(j + 1)) = f /. 1 & (GoB f) * ((i + 1),(j + 1)) = f /. 2 ) or ( (GoB f) * (i,(j + 1)) = f /. 2 & (GoB f) * ((i + 1),(j + 1)) = f /. 1 ) ) by A17, A39, SPPOL_1:8;
hence f /. (1 + 1) = (GoB f) * ((i + 1),(j + 1)) by A42, A43, Th36; :: thesis:
thus f /. 1 = (GoB f) * (i,(j + 1)) by A10, A40, A46, A41, A44, SPPOL_1:8; :: thesis:
thus f /. (1 + 2) = (GoB f) * ((i + 1),j) by A17, A39, A45, A42, A44, SPPOL_1:8; :: thesis:

end;

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

A49: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A16, A47, TOPREAL1:def 3;
then A50: ( ( (GoB f) * (i,(j + 1)) = f /. 1 & (GoB f) * ((i + 1),(j + 1)) = f /. 2 ) or ( (GoB f) * (i,(j + 1)) = f /. 2 & (GoB f) * ((i + 1),(j + 1)) = f /. 1 ) ) by A17, A47, SPPOL_1:8;
A51: 2 < k1 + 1 by A48, NAT_1:13;
then A52: f /. (k1 + 1) <> f /. 2 by A9, Th37;
LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by A8, A9, TOPREAL1:def 3;
then A53: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. k1 & (GoB f) * ((i + 1),j) = f /. (k1 + 1) ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. (k1 + 1) & (GoB f) * ((i + 1),j) = f /. k1 ) ) by A10, SPPOL_1:8;
A54: f /. k1 <> f /. 2 by A11, A48, Th36;
hence f /. 1 = (GoB f) * ((i + 1),(j + 1)) by A17, A47, A49, A53, A52, SPPOL_1:8; :: thesis:
thus f /. 2 = (GoB f) * (i,(j + 1)) by A17, A47, A49, A53, A54, A52, SPPOL_1:8; :: thesis:
A55: k1 > 1 by A48, XXREAL_0:2;
then A56: k1 + 1 > 1 by NAT_1:13;
then k1 + 1 = len f by A9, A11, A48, A50, A53, A55, A51, Th37, Th38;
then k1 + 1 = ((len f) -' 1) + 1 by A56, XREAL_1:235;
hence f /. ((len f) -' 1) = (GoB f) * ((i + 1),j) by A11, A48, A50, A53, A55, Th36; :: thesis:

end;

case k1 = k2 ; :: thesis:

then A57: ( (GoB f) * ((i + 1),j) = (GoB f) * (i,(j + 1)) or (GoB f) * ((i + 1),j) = (GoB f) * ((i + 1),(j + 1)) ) by A10, A17, SPPOL_1:8;
A58: [(i + 1),(j + 1)] in Indices (GoB f) by A2, A4, A7, A14, MATRIX_0:30;
( [i,(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) ) by A1, A2, A3, A4, A7, A14, A13, MATRIX_0:30;
then ( j = j + 1 or i = i + 1 ) by A57, A58, GOBOARD1:5;
hence contradiction ; :: thesis:

end;

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

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

end;

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

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

end;

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