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 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;

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 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 :: 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) )

hence
left_cell (f,i) = right_cell ((Rev f),j)
by A1, A4, GOBOARD5:def 7; :: thesis: verum( 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 ( b_{1} = b_{3} & b_{2} + 1 = b_{4} & right_cell ((Rev f),j) = cell ((GoB f),(b_{1} -' 1),b_{2}) ) & not ( b_{1} + 1 = b_{3} & b_{2} = b_{4} & right_cell ((Rev f),j) = cell ((GoB f),b_{1},b_{2}) ) & not ( b_{1} = b_{3} + 1 & b_{2} = b_{4} & right_cell ((Rev f),j) = cell ((GoB f),b_{3},(b_{4} -' 1)) ) implies ( b_{1} = b_{3} & b_{2} = b_{4} + 1 & right_cell ((Rev f),j) = cell ((GoB f),b_{1},b_{4}) ) )

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_{1} = b_{3} & b_{2} + 1 = b_{4} & right_cell ((Rev f),j) = cell ((GoB f),(b_{1} -' 1),b_{2}) ) or ( b_{1} + 1 = b_{3} & b_{2} = b_{4} & right_cell ((Rev f),j) = cell ((GoB f),b_{1},b_{2}) ) or ( b_{1} = b_{3} + 1 & b_{2} = b_{4} & right_cell ((Rev f),j) = cell ((GoB f),b_{3},(b_{4} -' 1)) ) or ( b_{1} = b_{3} & b_{2} = b_{4} + 1 & right_cell ((Rev f),j) = cell ((GoB f),b_{1},b_{4}) ) )

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_0:32;

then A15: (i1 -' 1) + 1 = i1 by XREAL_1:235;

1 <= j1 by A7, MATRIX_0:32;

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;

end;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

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_0:32;

then A15: (i1 -' 1) + 1 = i1 by XREAL_1:235;

1 <= j1 by A7, MATRIX_0:32;

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 A17, SEQM_3:41;

end;

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;