let n be Nat; :: thesis: for f being FinSequence st n <> 0 & f in Permutations n holds
Rev f in Permutations n
let f be FinSequence; :: thesis: ( n <> 0 & f in Permutations n implies Rev f in Permutations n )
assume A1: ( n <> 0 & f in Permutations n ) ; :: thesis: Rev f in Permutations n
then A2: f is Permutation of (Seg n) by MATRIX_2:def 11;
A3: Seg n <> {} by A1;
A4: Rev f is one-to-one by A2;
A5: rng f = Seg n by A2, FUNCT_2:def 3;
A6: ( dom f = dom (Rev f) & rng f = rng (Rev f) ) by FINSEQ_5:60;
then ( dom (Rev f) = Seg n & rng (Rev f) = Seg n ) by A2, A3, FUNCT_2:def 1, FUNCT_2:def 3;
then reconsider g = Rev f as FinSequence-like Function of (Seg n),(Seg n) by FUNCT_2:4;
g is onto by A5, A6, FUNCT_2:def 3;
then g is bijective by A4;
hence Rev f in Permutations n by MATRIX_2:def 11; :: thesis: verum