let f be non constant standard special_circular_sequence; :: thesis: for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds
left_cell (f,i) = right_cell ((Rev f),j)

let i, j be Nat; :: thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell (f,i) = right_cell ((Rev f),j) )
assume that
A1: i >= 1 and
A2: j >= 1 and
A3: i + j = len f ; :: thesis: left_cell (f,i) = right_cell ((Rev f),j)
A4: i + 1 <= len f by ;
len f = len (Rev f) by FINSEQ_5:def 3;
then A5: j + 1 <= len (Rev f) by ;
A6: GoB (Rev f) = GoB f by Lm1;
now :: thesis: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. i = (GoB f) * (i1,j1) & f /. (i + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell ((Rev f),j) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & right_cell ((Rev f),j) = cell ((GoB f),i1,j2) )
let i1, j1, i2, j2 be Nat; :: thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. i = (GoB f) * (i1,j1) & f /. (i + 1) = (GoB f) * (i2,j2) & not ( b1 = b3 & b2 + 1 = b4 & right_cell ((Rev f),j) = cell ((GoB f),(b1 -' 1),b2) ) & not ( b1 + 1 = b3 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b1,b2) ) & not ( b1 = b3 + 1 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b3,(b4 -' 1)) ) implies ( b1 = b3 & b2 = b4 + 1 & right_cell ((Rev f),j) = cell ((GoB f),b1,b4) ) )
assume that
A7: [i1,j1] in Indices (GoB f) and
A8: [i2,j2] in Indices (GoB f) and
A9: f /. i = (GoB f) * (i1,j1) and
A10: f /. (i + 1) = (GoB f) * (i2,j2) ; :: thesis: ( ( b1 = b3 & b2 + 1 = b4 & right_cell ((Rev f),j) = cell ((GoB f),(b1 -' 1),b2) ) or ( b1 + 1 = b3 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b1,b2) ) or ( b1 = b3 + 1 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b3,(b4 -' 1)) ) or ( b1 = b3 & b2 = b4 + 1 & right_cell ((Rev f),j) = cell ((GoB f),b1,b4) ) )
1 <= i + 1 by NAT_1:11;
then A11: i + 1 in dom f by ;
(i + 1) + j = (len f) + 1 by A3;
then A12: (Rev f) /. j = (GoB f) * (i2,j2) by ;
i <= len f by ;
then A13: i in dom f by ;
(j + 1) + i = (len f) + 1 by A3;
then A14: (Rev f) /. (j + 1) = (GoB f) * (i1,j1) by ;
1 <= i1 by ;
then A15: (i1 -' 1) + 1 = i1 by XREAL_1:235;
1 <= j1 by ;
then A16: (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;
f is_sequence_on GoB f by GOBOARD5:def 5;
then |.(i1 - i2).| + |.(j1 - j2).| = 1 by A7, A8, A9, A10, A11, A13;
then A17: ( ( |.(i19 - i29).| = 1 & j1 = j2 ) or ( |.(j19 - j29).| = 1 & i1 = i2 ) ) by SEQM_3:42;
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 ;
case ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1)
hence right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:30; :: thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: right_cell ((Rev f),j) = cell ((GoB f),i1,j1)
hence right_cell ((Rev f),j) = cell ((GoB f),i1,j1) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:29; :: thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1))
hence right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1)) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:28; :: thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: right_cell ((Rev f),j) = cell ((GoB f),i1,j2)
hence right_cell ((Rev f),j) = cell ((GoB f),i1,j2) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:27; :: thesis: verum
end;
end;
end;
hence left_cell (f,i) = right_cell ((Rev f),j) by ; :: thesis: verum