theorem Th5: :: MATRIX_9:5

for n being Nat
for f being FinSequence st n <> 0 & f in Permutations n holds
Rev f in Permutations n