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) & (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in L~ f holds
ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) )

let f be V8() standard special_circular_sequence; :: thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in L~ f implies ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) ) )

set mi = (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1))));
assume that
A1: ( 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) ) and
A2: (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in L~ f ; :: thesis: ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) )

L~ f = union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by TOPREAL1:def 4;
then consider x being set such that
A3: (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in x and
A4: x in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by ;
consider k being Nat such that
A5: x = LSeg (f,k) and
A6: 1 <= k and
A7: k + 1 <= len f by A4;
A8: f is_sequence_on GoB f by GOBOARD5:def 5;
A9: (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in LSeg ((f /. k),(f /. (k + 1))) by ;
k <= k + 1 by NAT_1:11;
then k <= len f by ;
then A10: k in dom f by ;
then consider i1, j1 being Nat such that
A11: [i1,j1] in Indices (GoB f) and
A12: f /. k = (GoB f) * (i1,j1) by ;
A13: 1 <= i1 by ;
take k ; :: thesis: ( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) )
thus ( 1 <= k & k + 1 <= len f ) by A6, A7; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k)
1 <= k + 1 by NAT_1:11;
then A14: k + 1 in dom f by ;
then consider i2, j2 being Nat such that
A15: [i2,j2] in Indices (GoB f) and
A16: f /. (k + 1) = (GoB f) * (i2,j2) by ;
A17: 1 <= i2 by ;
A18: j2 <= width (GoB f) by ;
|.(i1 - i2).| + |.(j1 - j2).| = 1 by ;
then A19: ( ( |.(i1 - i2).| = 1 & j1 = j2 ) or ( |.(j1 - j2).| = 1 & i1 = i2 ) ) by SEQM_3:42;
A20: i1 <= len (GoB f) by ;
A21: j1 <= width (GoB f) by ;
A22: 1 <= j1 by ;
A23: i2 <= len (GoB f) by ;
A24: 1 <= j2 by ;
per cases ( ( j1 = j2 & i1 = i2 + 1 ) or ( j1 = j2 & i1 + 1 = i2 ) or ( j1 = j2 + 1 & i1 = i2 ) or ( j1 + 1 = j2 & i1 = i2 ) ) by ;
suppose A25: ( j1 = j2 & i1 = i2 + 1 ) ; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k)
then (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in LSeg (((GoB f) * (i2,j2)),((GoB f) * ((i2 + 1),j2))) by ;
hence LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) by A1, A20, A17, A24, A18, A25, Th28; :: thesis: verum
end;
suppose A26: ( j1 = j2 & i1 + 1 = i2 ) ; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k)
then (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in LSeg (((GoB f) * (i1,j1)),((GoB f) * ((i1 + 1),j1))) by ;
hence LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) by A1, A13, A22, A21, A23, A26, Th28; :: thesis: verum
end;
suppose A27: ( j1 = j2 + 1 & i1 = i2 ) ; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k)
then ( i = i2 & j = j2 ) by A1, A12, A16, A13, A20, A21, A24, A9, Th25;
hence LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) by ; :: thesis: verum
end;
suppose A28: ( j1 + 1 = j2 & i1 = i2 ) ; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k)
then ( i = i1 & j = j1 ) by A1, A12, A16, A13, A20, A22, A18, A9, Th25;
hence LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) by ; :: thesis: verum
end;
end;