let n be Nat; :: thesis: Rev (idseq n) in Permutations n
reconsider f = idseq n as one-to-one FinSequence-like Function of (Seg n),(Seg n) ;
dom f = dom (Rev f) by FINSEQ_5:57;
then A1: dom (Rev f) = Seg n by RELAT_1:45;
A2: rng (idseq n) = Seg n by FUNCT_2:def 3;
then rng (Rev f) c= Seg n by FINSEQ_5:57;
then reconsider g = Rev f as FinSequence-like Function of (Seg n),(Seg n) by A1, FUNCT_2:2;
rng f = rng (Rev f) by FINSEQ_5:57;
then g is onto by A2, FUNCT_2:def 3;
hence Rev (idseq n) in Permutations n by MATRIX_1:def 12; :: thesis: verum