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

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