let n be Nat; :: thesis: Rev (idseq n) is Permutation of (Seg n)
reconsider f = idseq n as one-to-one FinSequence-like Function of (Seg n),(Seg n) by FINSEQ_2:55;
A1: dom (Rev (idseq n)) = dom (idseq n) by FINSEQ_5:57
.= dom (id (Seg n)) by FINSEQ_2:def 1
.= Seg n ;
A2: rng (idseq n) = rng (id (Seg n)) by FINSEQ_2:def 1
.= Seg n ;
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) is Permutation of (Seg n) ; :: thesis: verum