let i, j be Nat; :: thesis: for f being V8() standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) holds
ex k being 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,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) )

let f be V8() standard special_circular_sequence; :: thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) implies ex k being 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,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) )

assume that
A1: ( 1 <= i & i <= len (GoB f) ) and
A2: 1 <= j and
A3: j + 1 < width (GoB f) and
A4: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f and
A5: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f ; :: thesis: ( ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) or ex k being 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,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) )

A6: 1 <= j + 1 by NAT_1:11;
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) by RLTOPSP1:69;
then consider k1 being Nat such that
A7: 1 <= k1 and
A8: k1 + 1 <= len f and
A9: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k1) by A1, A2, A3, A4, Th39;
A10: k1 < len f by ;
A11: now :: thesis: ( not k1 > 1 or k1 = 2 or k1 > 2 )
assume k1 > 1 ; :: thesis: ( k1 = 2 or k1 > 2 )
then k1 >= 1 + 1 by NAT_1:13;
hence ( k1 = 2 or k1 > 2 ) by XXREAL_0:1; :: thesis: verum
end;
A12: j < width (GoB f) by ;
A13: j + (1 + 1) = (j + 1) + 1 ;
then A14: 1 <= j + 2 by NAT_1:11;
A15: j + 2 <= width (GoB f) by ;
(1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * (i,(j + 2)))) in LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) by RLTOPSP1:69;
then consider k2 being Nat such that
A16: 1 <= k2 and
A17: k2 + 1 <= len f and
A18: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) = LSeg (f,k2) by A1, A5, A6, A13, A15, Th39;
A19: k2 < len f by ;
A20: now :: thesis: ( not k2 > 1 or k2 = 2 or k2 > 2 )
assume k2 > 1 ; :: thesis: ( k2 = 2 or k2 > 2 )
then k2 >= 1 + 1 by NAT_1:13;
hence ( k2 = 2 or k2 > 2 ) by XXREAL_0:1; :: thesis: verum
end;
A21: ( k1 = 1 or k1 > 1 ) by ;
now :: thesis: ( ( k1 = 1 & k2 = 2 & 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) ) or ( k1 = 1 & k2 > 2 & f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( k2 = 1 & k1 = 2 & 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) ) or ( k2 = 1 & k1 > 2 & f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) or ( k1 = k2 & contradiction ) or ( k1 > 1 & k2 > k1 & 1 <= k1 & k1 + 1 < len f & f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) ) or ( k2 > 1 & k1 > k2 & 1 <= k2 & k2 + 1 < len f & f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) ) )
per cases ( ( k1 = 1 & k2 = 2 ) or ( k1 = 1 & k2 > 2 ) or ( k2 = 1 & k1 = 2 ) or ( k2 = 1 & k1 > 2 ) or k1 = k2 or ( k1 > 1 & k2 > k1 ) or ( k2 > 1 & k1 > k2 ) ) by ;
case that A22: k1 = 1 and
A23: k2 = 2 ; :: thesis: ( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) )
A24: LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1))) by ;
then A25: ( ( (GoB f) * (i,(j + 1)) = f /. 2 & (GoB f) * (i,(j + 2)) = f /. (2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (2 + 1) & (GoB f) * (i,(j + 2)) = f /. 2 ) ) by ;
thus ( 1 <= 1 & 1 + 1 < len f ) by ; :: thesis: ( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) )
A26: 3 < len f by ;
then A27: f /. 1 <> f /. 3 by Th36;
A28: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by ;
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 ;
hence f /. (1 + 1) = (GoB f) * (i,(j + 1)) by ; :: thesis: ( f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) )
thus f /. 1 = (GoB f) * (i,j) by ; :: thesis: f /. (1 + 2) = (GoB f) * (i,(j + 2))
thus f /. (1 + 2) = (GoB f) * (i,(j + 2)) by ; :: thesis: verum
end;
case that A30: k1 = 1 and
A31: k2 > 2 ; :: thesis: ( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) )
A32: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by ;
then A33: ( ( (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 ;
A34: 2 < k2 + 1 by ;
then A35: f /. (k2 + 1) <> f /. 2 by ;
LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by ;
then A36: ( ( (GoB f) * (i,(j + 1)) = f /. k2 & (GoB f) * (i,(j + 2)) = f /. (k2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k2 + 1) & (GoB f) * (i,(j + 2)) = f /. k2 ) ) by ;
A37: f /. k2 <> f /. 2 by ;
hence f /. 1 = (GoB f) * (i,(j + 1)) by ; :: thesis: ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) )
thus f /. 2 = (GoB f) * (i,j) by ; :: thesis: f /. ((len f) -' 1) = (GoB f) * (i,(j + 2))
A38: k2 > 1 by ;
then A39: k2 + 1 > 1 by NAT_1:13;
then k2 + 1 = len f by A17, A19, A31, A33, A36, A38, A34, Th37, Th38;
then k2 + 1 = ((len f) -' 1) + 1 by ;
hence f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) by A19, A31, A33, A36, A38, Th36; :: thesis: verum
end;
case that A40: k2 = 1 and
A41: k1 = 2 ; :: thesis: ( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) )
A42: LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1))) by ;
then A43: ( ( (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 ;
thus ( 1 <= 1 & 1 + 1 < len f ) by ; :: thesis: ( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) )
A44: 3 < len f by ;
then A45: f /. 1 <> f /. 3 by Th36;
A46: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by ;
then A47: ( ( (GoB f) * (i,(j + 2)) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * (i,(j + 2)) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by ;
hence f /. (1 + 1) = (GoB f) * (i,(j + 1)) by ; :: thesis: ( f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) )
thus f /. 1 = (GoB f) * (i,(j + 2)) by ; :: thesis: f /. (1 + 2) = (GoB f) * (i,j)
thus f /. (1 + 2) = (GoB f) * (i,j) by ; :: thesis: verum
end;
case that A48: k2 = 1 and
A49: k1 > 2 ; :: thesis: ( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )
A50: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by ;
then A51: ( ( (GoB f) * (i,(j + 2)) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * (i,(j + 2)) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by ;
A52: 2 < k1 + 1 by ;
then A53: f /. (k1 + 1) <> f /. 2 by ;
LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by ;
then A54: ( ( (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 ;
A55: f /. k1 <> f /. 2 by ;
hence f /. 1 = (GoB f) * (i,(j + 1)) by ; :: thesis: ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )
thus f /. 2 = (GoB f) * (i,(j + 2)) by ; :: thesis: f /. ((len f) -' 1) = (GoB f) * (i,j)
A56: k1 > 1 by ;
then A57: k1 + 1 > 1 by NAT_1:13;
then k1 + 1 = len f by A8, A10, A49, A51, A54, A56, A52, Th37, Th38;
then k1 + 1 = ((len f) -' 1) + 1 by ;
hence f /. ((len f) -' 1) = (GoB f) * (i,j) by A10, A49, A51, A54, A56, Th36; :: thesis: verum
end;
case k1 = k2 ; :: thesis: contradiction
then A58: ( (GoB f) * (i,j) = (GoB f) * (i,(j + 2)) or (GoB f) * (i,j) = (GoB f) * (i,(j + 1)) ) by ;
A59: [i,(j + 2)] in Indices (GoB f) by ;
( [i,j] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by ;
then ( j = j + 1 or j = j + 2 ) by ;
hence contradiction ; :: thesis: verum
end;
case that A60: k1 > 1 and
A61: k2 > k1 ; :: thesis: ( 1 <= k1 & k1 + 1 < len f & f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) )
A62: ( 1 < k1 + 1 & k1 + 1 < k2 + 1 ) by ;
A63: k1 < k2 + 1 by ;
then A64: f /. k1 <> f /. (k2 + 1) by ;
A65: k1 + 1 <= k2 by ;
LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by ;
then A66: ( ( (GoB f) * (i,(j + 1)) = f /. k2 & (GoB f) * (i,(j + 2)) = f /. (k2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k2 + 1) & (GoB f) * (i,(j + 2)) = f /. k2 ) ) by ;
A67: k2 < len f by ;
then A68: f /. k1 <> f /. k2 by ;
A69: LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by ;
then ( ( (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 ;
then k1 + 1 >= k2 by A17, A60, A61, A66, A63, A67, A62, Th37;
then A70: k1 + 1 = k2 by ;
hence ( 1 <= k1 & k1 + 1 < len f ) by ; :: thesis: ( f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) )
thus f /. (k1 + 1) = (GoB f) * (i,(j + 1)) by ; :: thesis: ( f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) )
thus f /. k1 = (GoB f) * (i,j) by ; :: thesis: f /. (k1 + 2) = (GoB f) * (i,(j + 2))
thus f /. (k1 + 2) = (GoB f) * (i,(j + 2)) by ; :: thesis: verum
end;
case that A71: k2 > 1 and
A72: k1 > k2 ; :: thesis: ( 1 <= k2 & k2 + 1 < len f & f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) )
A73: ( 1 < k2 + 1 & k2 + 1 < k1 + 1 ) by ;
A74: k2 < k1 + 1 by ;
then A75: f /. k2 <> f /. (k1 + 1) by ;
A76: k2 + 1 <= k1 by ;
LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by ;
then A77: ( ( (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 ;
A78: k1 < len f by ;
then A79: f /. k2 <> f /. k1 by ;
A80: LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by ;
then ( ( (GoB f) * (i,(j + 2)) = f /. k2 & (GoB f) * (i,(j + 1)) = f /. (k2 + 1) ) or ( (GoB f) * (i,(j + 2)) = f /. (k2 + 1) & (GoB f) * (i,(j + 1)) = f /. k2 ) ) by ;
then k2 + 1 >= k1 by A8, A71, A72, A77, A74, A78, A73, Th37;
then A81: k2 + 1 = k1 by ;
hence ( 1 <= k2 & k2 + 1 < len f ) by ; :: thesis: ( f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) )
thus f /. (k2 + 1) = (GoB f) * (i,(j + 1)) by ; :: thesis: ( f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) )
thus f /. k2 = (GoB f) * (i,(j + 2)) by ; :: thesis: f /. (k2 + 2) = (GoB f) * (i,j)
thus f /. (k2 + 2) = (GoB f) * (i,j) by ; :: thesis: verum
end;
end;
end;
hence ( ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) or ex k being 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,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) ) ; :: thesis: verum