let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell (f,i) = right_cell ((Rev f),j)
let i, j be Element of 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 A2, A3, XREAL_1:6;
len f = len (Rev f) by FINSEQ_5:def 3;
then A5: j + 1 <= len (Rev f) by A1, A3, XREAL_1:6;
A6: GoB (Rev f) = GoB f by Lm1;

now

let i1, j1, i2, j2 be Element of 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 ( b₁ = b₃ & b₂ + 1 = b₄ & right_cell ((Rev f),j) = cell ((GoB f),(b₁ -' 1),b₂) ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & right_cell ((Rev f),j) = cell ((GoB f),b₁,b₂) ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & right_cell ((Rev f),j) = cell ((GoB f),b₃,(b₄ -' 1)) ) implies ( b₁ = b₃ & b₂ = b₄ + 1 & right_cell ((Rev f),j) = cell ((GoB f),b₁,b₄) ) )
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: ( ( b₁ = b₃ & b₂ + 1 = b₄ & right_cell ((Rev f),j) = cell ((GoB f),(b₁ -' 1),b₂) ) or ( b₁ + 1 = b₃ & b₂ = b₄ & right_cell ((Rev f),j) = cell ((GoB f),b₁,b₂) ) or ( b₁ = b₃ + 1 & b₂ = b₄ & right_cell ((Rev f),j) = cell ((GoB f),b₃,(b₄ -' 1)) ) or ( b₁ = b₃ & b₂ = b₄ + 1 & right_cell ((Rev f),j) = cell ((GoB f),b₁,b₄) ) )
1 <= i + 1 by NAT_1:11;
then A11: i + 1 in dom f by A4, FINSEQ_3:25;
(i + 1) + j = (len f) + 1 by A3;
then A12: (Rev f) /. j = (GoB f) * (i2,j2) by A10, A11, FINSEQ_5:66;
i <= len f by A4, NAT_1:13;
then A13: i in dom f by A1, FINSEQ_3:25;
(j + 1) + i = (len f) + 1 by A3;
then A14: (Rev f) /. (j + 1) = (GoB f) * (i1,j1) by A9, A13, FINSEQ_5:66;
1 <= i1 by A7, MATRIX_1:38;
then A15: (i1 -' 1) + 1 = i1 by XREAL_1:235;
1 <= j1 by A7, MATRIX_1:38;
then A16: (j1 -' 1) + 1 = j1 by XREAL_1:235;
reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL ;
f is_sequence_on GoB f by GOBOARD5:def 5;
then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A7, A8, A9, A10, A11, A13, GOBOARD1:def 9;
then A17: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (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 A17, SEQM_3:41;

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 A1, A4, GOBOARD5:def 7; :: thesis: verum