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 ((Rev f),i) = right_cell (f,j)
let i, j be Nat; :: thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell ((Rev f),i) = right_cell (f,j) )
A1: len (Rev f) = len f by FINSEQ_5:def 3;
Rev (Rev f) = f ;
hence ( i >= 1 & j >= 1 & i + j = len f implies left_cell ((Rev f),i) = right_cell (f,j) ) by A1, Th8; :: thesis: verum