for n being Nat holds Rev (idseq n) is Permutation of (Seg n)