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