let f be non constant standard special_circular_sequence; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds

ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

A3: f is_sequence_on GoB f by GOBOARD5:def 5;

k <= len f by A2, NAT_1:13;

then A4: k in dom f by A1, FINSEQ_3:25;

then consider i1, j1 being Nat such that

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

A6: f /. k = (GoB f) * (i1,j1) by A3;

1 <= k + 1 by NAT_1:11;

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

then consider i2, j2 being Nat such that

A8: [i2,j2] in Indices (GoB f) and

A9: f /. (k + 1) = (GoB f) * (i2,j2) by A3;

1 <= i1 by A5, MATRIX_0:32;

then A10: (i1 -' 1) + 1 = i1 by XREAL_1:235;

1 <= j1 by A5, MATRIX_0:32;

then A11: (j1 -' 1) + 1 = j1 by XREAL_1:235;

reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def 1;

|.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A4, A5, A6, A7, A8, A9;

then A12: ( ( |.(i19 - i29).| = 1 & j1 = j2 ) or ( |.(j19 - j29).| = 1 & i1 = i2 ) ) by SEQM_3:42;

A13: i1 <= len (GoB f) by A5, MATRIX_0:32;

A14: j1 <= width (GoB f) by A5, MATRIX_0:32;

ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

A3: f is_sequence_on GoB f by GOBOARD5:def 5;

k <= len f by A2, NAT_1:13;

then A4: k in dom f by A1, FINSEQ_3:25;

then consider i1, j1 being Nat such that

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

A6: f /. k = (GoB f) * (i1,j1) by A3;

1 <= k + 1 by NAT_1:11;

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

then consider i2, j2 being Nat such that

A8: [i2,j2] in Indices (GoB f) and

A9: f /. (k + 1) = (GoB f) * (i2,j2) by A3;

1 <= i1 by A5, MATRIX_0:32;

then A10: (i1 -' 1) + 1 = i1 by XREAL_1:235;

1 <= j1 by A5, MATRIX_0:32;

then A11: (j1 -' 1) + 1 = j1 by XREAL_1:235;

reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def 1;

|.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A4, A5, A6, A7, A8, A9;

then A12: ( ( |.(i19 - i29).| = 1 & j1 = j2 ) or ( |.(j19 - j29).| = 1 & i1 = i2 ) ) by SEQM_3:42;

A13: i1 <= len (GoB f) by A5, MATRIX_0:32;

A14: j1 <= width (GoB f) by A5, MATRIX_0:32;

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

end;

suppose A15:
( i1 = i2 & j1 + 1 = j2 )
; :: thesis: ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

take
i1 -' 1
; :: thesis: ex j being Nat st

( i1 -' 1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),(i1 -' 1),j) = left_cell (f,k) )

take j1 ; :: thesis: ( i1 -' 1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) )

i1 -' 1 <= i1 by NAT_D:35;

hence i1 -' 1 <= len (GoB f) by A13, XXREAL_0:2; :: thesis: ( j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) )

thus j1 <= width (GoB f) by A5, MATRIX_0:32; :: thesis: cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k)

thus cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A15, GOBOARD5:27; :: thesis: verum

end;( i1 -' 1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),(i1 -' 1),j) = left_cell (f,k) )

take j1 ; :: thesis: ( i1 -' 1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) )

i1 -' 1 <= i1 by NAT_D:35;

hence i1 -' 1 <= len (GoB f) by A13, XXREAL_0:2; :: thesis: ( j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) )

thus j1 <= width (GoB f) by A5, MATRIX_0:32; :: thesis: cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k)

thus cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A15, GOBOARD5:27; :: thesis: verum

suppose A16:
( i1 + 1 = i2 & j1 = j2 )
; :: thesis: ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

take
i1
; :: thesis: ex j being Nat st

( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) )

take j1 ; :: thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) )

thus i1 <= len (GoB f) by A5, MATRIX_0:32; :: thesis: ( j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) )

thus j1 <= width (GoB f) by A5, MATRIX_0:32; :: thesis: cell ((GoB f),i1,j1) = left_cell (f,k)

thus cell ((GoB f),i1,j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A16, GOBOARD5:28; :: thesis: verum

end;( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) )

take j1 ; :: thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) )

thus i1 <= len (GoB f) by A5, MATRIX_0:32; :: thesis: ( j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) )

thus j1 <= width (GoB f) by A5, MATRIX_0:32; :: thesis: cell ((GoB f),i1,j1) = left_cell (f,k)

thus cell ((GoB f),i1,j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A16, GOBOARD5:28; :: thesis: verum

suppose A17:
( i1 = i2 + 1 & j1 = j2 )
; :: thesis: ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

take
i2
; :: thesis: ex j being Nat st

( i2 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i2,j) = left_cell (f,k) )

take j1 -' 1 ; :: thesis: ( i2 <= len (GoB f) & j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) )

thus i2 <= len (GoB f) by A8, MATRIX_0:32; :: thesis: ( j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) )

j1 -' 1 <= j1 by NAT_D:35;

hence j1 -' 1 <= width (GoB f) by A14, XXREAL_0:2; :: thesis: cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k)

thus cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A17, GOBOARD5:29; :: thesis: verum

end;( i2 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i2,j) = left_cell (f,k) )

take j1 -' 1 ; :: thesis: ( i2 <= len (GoB f) & j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) )

thus i2 <= len (GoB f) by A8, MATRIX_0:32; :: thesis: ( j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) )

j1 -' 1 <= j1 by NAT_D:35;

hence j1 -' 1 <= width (GoB f) by A14, XXREAL_0:2; :: thesis: cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k)

thus cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A17, GOBOARD5:29; :: thesis: verum

suppose A18:
( i1 = i2 & j1 = j2 + 1 )
; :: thesis: ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )

take
i1
; :: thesis: ex j being Nat st

( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) )

take j2 ; :: thesis: ( i1 <= len (GoB f) & j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) )

thus i1 <= len (GoB f) by A5, MATRIX_0:32; :: thesis: ( j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) )

thus j2 <= width (GoB f) by A8, MATRIX_0:32; :: thesis: cell ((GoB f),i1,j2) = left_cell (f,k)

thus cell ((GoB f),i1,j2) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A18, GOBOARD5:30; :: thesis: verum

end;( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) )

take j2 ; :: thesis: ( i1 <= len (GoB f) & j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) )

thus i1 <= len (GoB f) by A5, MATRIX_0:32; :: thesis: ( j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) )

thus j2 <= width (GoB f) by A8, MATRIX_0:32; :: thesis: cell ((GoB f),i1,j2) = left_cell (f,k)

thus cell ((GoB f),i1,j2) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A18, GOBOARD5:30; :: thesis: verum