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

ex k being Nat st

( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )

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

( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) ) )

set mi = (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j)));

assume that

A1: ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j <= width (GoB f) ) and

A2: (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in L~ f ; :: thesis: ex k being Nat st

( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = 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 + 1),j))) in x and

A4: x in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A2, TARSKI:def 4;

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 + 1),j))) in LSeg ((f /. k),(f /. (k + 1))) by A3, A5, A6, A7, TOPREAL1:def 3;

k <= k + 1 by NAT_1:11;

then k <= len f by A7, XXREAL_0:2;

then A10: k in dom f by A6, FINSEQ_3:25;

then consider i1, j1 being Nat such that

A11: [i1,j1] in Indices (GoB f) and

A12: f /. k = (GoB f) * (i1,j1) by A8, GOBOARD1:def 9;

A13: 1 <= j1 by A11, MATRIX_0:32;

take k ; :: thesis: ( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )

thus ( 1 <= k & k + 1 <= len f ) by A6, A7; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)

1 <= k + 1 by NAT_1:11;

then A14: k + 1 in dom f by A7, FINSEQ_3:25;

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 A8, GOBOARD1:def 9;

A17: 1 <= j2 by A15, MATRIX_0:32;

A18: i2 <= len (GoB f) by A15, MATRIX_0:32;

|.(j1 - j2).| + |.(i1 - i2).| = 1 by A8, A10, A11, A12, A14, A15, A16, GOBOARD1:def 9;

then A19: ( ( |.(j1 - j2).| = 1 & i1 = i2 ) or ( |.(i1 - i2).| = 1 & j1 = j2 ) ) by SEQM_3:42;

A20: j1 <= width (GoB f) by A11, MATRIX_0:32;

A21: i1 <= len (GoB f) by A11, MATRIX_0:32;

A22: 1 <= i1 by A11, MATRIX_0:32;

A23: j2 <= width (GoB f) by A15, MATRIX_0:32;

A24: 1 <= i2 by A15, MATRIX_0:32;

ex k being Nat st

( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )

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

( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) ) )

set mi = (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j)));

assume that

A1: ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j <= width (GoB f) ) and

A2: (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in L~ f ; :: thesis: ex k being Nat st

( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = 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 + 1),j))) in x and

A4: x in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A2, TARSKI:def 4;

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 + 1),j))) in LSeg ((f /. k),(f /. (k + 1))) by A3, A5, A6, A7, TOPREAL1:def 3;

k <= k + 1 by NAT_1:11;

then k <= len f by A7, XXREAL_0:2;

then A10: k in dom f by A6, FINSEQ_3:25;

then consider i1, j1 being Nat such that

A11: [i1,j1] in Indices (GoB f) and

A12: f /. k = (GoB f) * (i1,j1) by A8, GOBOARD1:def 9;

A13: 1 <= j1 by A11, MATRIX_0:32;

take k ; :: thesis: ( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )

thus ( 1 <= k & k + 1 <= len f ) by A6, A7; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)

1 <= k + 1 by NAT_1:11;

then A14: k + 1 in dom f by A7, FINSEQ_3:25;

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 A8, GOBOARD1:def 9;

A17: 1 <= j2 by A15, MATRIX_0:32;

A18: i2 <= len (GoB f) by A15, MATRIX_0:32;

|.(j1 - j2).| + |.(i1 - i2).| = 1 by A8, A10, A11, A12, A14, A15, A16, GOBOARD1:def 9;

then A19: ( ( |.(j1 - j2).| = 1 & i1 = i2 ) or ( |.(i1 - i2).| = 1 & j1 = j2 ) ) by SEQM_3:42;

A20: j1 <= width (GoB f) by A11, MATRIX_0:32;

A21: i1 <= len (GoB f) by A11, MATRIX_0:32;

A22: 1 <= i1 by A11, MATRIX_0:32;

A23: j2 <= width (GoB f) by A15, MATRIX_0:32;

A24: 1 <= i2 by A15, MATRIX_0:32;

per cases
( ( i1 = i2 & j1 = j2 + 1 ) or ( i1 = i2 & j1 + 1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) )
by A19, SEQM_3:41;

end;

suppose A25:
( i1 = i2 & j1 = j2 + 1 )
; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)

then
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in LSeg (((GoB f) * (i2,j2)),((GoB f) * (i2,(j2 + 1))))
by A3, A5, A6, A7, A12, A16, TOPREAL1:def 3;

hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A1, A20, A17, A24, A18, A25, Th27; :: thesis: verum

end;hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A1, A20, A17, A24, A18, A25, Th27; :: thesis: verum

suppose A26:
( i1 = i2 & j1 + 1 = j2 )
; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)

then
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in LSeg (((GoB f) * (i1,j1)),((GoB f) * (i1,(j1 + 1))))
by A3, A5, A6, A7, A12, A16, TOPREAL1:def 3;

hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A1, A13, A22, A21, A23, A26, Th27; :: thesis: verum

end;hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A1, A13, A22, A21, A23, A26, Th27; :: thesis: verum

suppose A27:
( i1 = i2 + 1 & j1 = j2 )
; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)

then
( j = j2 & i = i2 )
by A1, A12, A16, A13, A20, A21, A24, A9, Th26;

hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A6, A7, A12, A16, A27, TOPREAL1:def 3; :: thesis: verum

end;hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A6, A7, A12, A16, A27, TOPREAL1:def 3; :: thesis: verum

suppose A28:
( i1 + 1 = i2 & j1 = j2 )
; :: thesis: LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)

then
( j = j1 & i = i1 )
by A1, A12, A16, A13, A20, A22, A18, A9, Th26;

hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A6, A7, A12, A16, A28, TOPREAL1:def 3; :: thesis: verum

end;hence LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) by A6, A7, A12, A16, A28, TOPREAL1:def 3; :: thesis: verum