theorem Th4: :: MATRIX_9:4

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