let i, j, k be Nat; for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds
( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) )
let f be standard special_circular_sequence; ( 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) implies ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) ) )
assume that
A1:
1 <= k
and
A2:
k + 1 <= len f
and
A3:
[(i + 1),j] in Indices (GoB f)
and
A4:
[(i + 1),(j + 1)] in Indices (GoB f)
and
A5:
f /. k = (GoB f) * ((i + 1),j)
and
A6:
f /. (k + 1) = (GoB f) * ((i + 1),(j + 1))
; ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) )
A7:
j < j + 1
by XREAL_1:29;
A8:
j + 1 <= (j + 1) + 1
by NAT_1:11;
hence left_cell (f,k) =
cell ((GoB f),((i + 1) -' 1),j)
by A1, A2, A3, A4, A5, A6, A7, Def7
.=
cell ((GoB f),i,j)
by NAT_D:34
;
right_cell (f,k) = cell ((GoB f),(i + 1),j)
thus
right_cell (f,k) = cell ((GoB f),(i + 1),j)
by A1, A2, A3, A4, A5, A6, A7, A8, Def6; verum