for n being Nat holds Rev (idseq n) in Permutations n