reconsider f = idseq 2 as one-to-one FinSequence-like Function of (Seg 2),(Seg 2) ;
f . 1 = (Rev f) . (len f)
by FINSEQ_5:62;
then A1:
(idseq 2) . 1 = (Rev (idseq 2)) . 2
by CARD_1:def 7;
f . (len f) = (Rev f) . 1
by FINSEQ_5:62;
then A2:
f . 2 = (Rev f) . 1
by CARD_1:def 7;
A3:
dom (Rev f) = dom f
by FINSEQ_5:57;
then A4:
dom (Rev f) = Seg 2
by RELAT_1:45;
then
( 1 in dom f & 2 in dom f )
by A3;
hence
( (Rev (idseq 2)) . 1 = 2 & (Rev (idseq 2)) . 2 = 1 )
by A1, A2, A3, A4, FUNCT_1:18; verum