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