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