let f be non constant standard special_circular_sequence; :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k )
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len f implies ex i, j being Element of 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 Element of 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:27;
then consider i1, j1 being Element of NAT such that
A5:
[i1,j1] in Indices (GoB f)
and
A6:
f /. k = (GoB f) * i1,j1
by A3, GOBOARD1:def 11;
1 <= k + 1
by NAT_1:11;
then A7:
k + 1 in dom f
by A2, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A8:
[i2,j2] in Indices (GoB f)
and
A9:
f /. (k + 1) = (GoB f) * i2,j2
by A3, GOBOARD1:def 11;
1 <= i1
by A5, MATRIX_1:39;
then A10:
(i1 -' 1) + 1 = i1
by XREAL_1:237;
1 <= j1
by A5, MATRIX_1:39;
then A11:
(j1 -' 1) + 1 = j1
by XREAL_1:237;
reconsider i1' = i1, i2' = i2, j1' = j1, j2' = j2 as Element of REAL ;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1
by A3, A4, A5, A6, A7, A8, A9, GOBOARD1:def 11;
then A12:
( ( abs (i1' - i2') = 1 & j1 = j2 ) or ( abs (j1' - j2') = 1 & i1 = i2 ) )
by GOBOARD1:2;
A13:
i1 <= len (GoB f)
by A5, MATRIX_1:39;
A14:
j1 <= width (GoB f)
by A5, MATRIX_1:39;
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, GOBOARD1:1;
suppose A15:
(
i1 = i2 &
j1 + 1
= j2 )
;
:: thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k )take
i1 -' 1
;
:: thesis: ex j being Element of 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_1:39;
:: thesis: cell (GoB f),(i1 -' 1),j1 = left_cell f,kthus
cell (GoB f),
(i1 -' 1),
j1 = left_cell f,
k
by A1, A2, A5, A6, A8, A9, A10, A15, GOBOARD5:28;
:: thesis: verum end; suppose A16:
(
i1 + 1
= i2 &
j1 = j2 )
;
:: thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k )take
i1
;
:: thesis: ex j being Element of 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_1:39;
:: thesis: ( j1 <= width (GoB f) & cell (GoB f),i1,j1 = left_cell f,k )thus
j1 <= width (GoB f)
by A5, MATRIX_1:39;
:: thesis: cell (GoB f),i1,j1 = left_cell f,kthus
cell (GoB f),
i1,
j1 = left_cell f,
k
by A1, A2, A5, A6, A8, A9, A11, A16, GOBOARD5:29;
:: thesis: verum end; suppose A17:
(
i1 = i2 + 1 &
j1 = j2 )
;
:: thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k )take
i2
;
:: thesis: ex j being Element of 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_1:39;
:: 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,kthus
cell (GoB f),
i2,
(j1 -' 1) = left_cell f,
k
by A1, A2, A5, A6, A8, A9, A11, A17, GOBOARD5:30;
:: thesis: verum end; suppose A18:
(
i1 = i2 &
j1 = j2 + 1 )
;
:: thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k )take
i1
;
:: thesis: ex j being Element of 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_1:39;
:: thesis: ( j2 <= width (GoB f) & cell (GoB f),i1,j2 = left_cell f,k )thus
j2 <= width (GoB f)
by A8, MATRIX_1:39;
:: thesis: cell (GoB f),i1,j2 = left_cell f,kthus
cell (GoB f),
i1,
j2 = left_cell f,
k
by A1, A2, A5, A6, A8, A9, A10, A18, GOBOARD5:31;
:: thesis: verum end;