set l = m + 1;
set k = (m + n) + 1;
A0: ( (m + n) + 1 = len (idseq ((m + n) + 1)) & len (idseq ((m + n) + 1)) = len (Rev (idseq ((m + n) + 1))) ) by FINSEQ_5:def 3;
( 1 <= m + 1 & m + 1 <= (m + 1) + n ) by NAT_1:11;
then m + 1 in dom (Rev (idseq ((m + n) + 1))) by A0, FINSEQ_3:25;
then (Rev (idseq ((m + n) + 1))) . (m + 1) = (idseq ((m + n) + 1)) . ((((m + n) + 1) - (m + 1)) + 1) by A0, FINSEQ_5:def 3
.= (idseq (m + (n + 1))) . (n + 1) ;
hence (Rev (idseq (m + (n + 1)))) . (m + 1) = n + 1 ; :: thesis: verum