theorem MATRIX94: :: NEWTON04:6

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