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 (Rev f),i = right_cell f,j
let i, j be Element of NAT ; :: thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell (Rev f),i = right_cell f,j )
( len (Rev f) = len f & Rev (Rev f) = f ) by FINSEQ_5:def 3, FINSEQ_6:29;
hence ( i >= 1 & j >= 1 & i + j = len f implies left_cell (Rev f),i = right_cell f,j ) by Th12; :: thesis: verum