let f be FinSequence; :: thesis: for i, j being Nat st i in dom f & i + j = (len f) + 1 holds
j in dom (Rev f)
let i, j be Nat; :: thesis: ( i in dom f & i + j = (len f) + 1 implies j in dom (Rev f) )
assume that
A1: i in dom f and
A2: i + j = (len f) + 1 ; :: thesis: j in dom (Rev f)
A3: ( dom f = Seg (len f) & dom f = dom (Rev f) ) by Th57, FINSEQ_1:def 3;
j = ((len f) - i) + 1 by A2;
hence j in dom (Rev f) by A1, A3, Th2; :: thesis: verum