reconsider f = idseq 2 as one-to-one FinSequence-like Function of (Seg 2),(Seg 2) ;
( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 ) by FINSEQ_5:65;
then A1: ( (idseq 2) . 1 = (Rev (idseq 2)) . 2 & f . 2 = (Rev f) . 1 ) by FINSEQ_1:def 18;
A2: ( dom (Rev f) = dom f & rng (Rev f) = rng f ) by FINSEQ_5:60;
then A3: dom (Rev f) = Seg 2 by RELAT_1:71;
then A4: 1 in dom f by A2;
2 in dom f by A2, A3;
hence ( (Rev (idseq 2)) . 1 = 2 & (Rev (idseq 2)) . 2 = 1 ) by A1, A2, A3, A4, FUNCT_1:35; :: thesis: verum