let i, j, k be Nat; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: ( 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 ;
:: thesis: 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; :: thesis: verum