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 that
A1: n <> 0 and
A2: f in Permutations n ; :: thesis: Rev f in Permutations n
A3: f is Permutation of (Seg n) by A2, MATRIX_1:def 12;
dom f = dom (Rev f) by FINSEQ_5:57;
then A4: dom (Rev f) = Seg n by A1, A3, FUNCT_2:def 1;
A5: rng f = rng (Rev f) by FINSEQ_5:57;
then rng (Rev f) = Seg n by A3, FUNCT_2:def 3;
then reconsider g = Rev f as FinSequence-like Function of (Seg n),(Seg n) by A4, FUNCT_2:2;
rng f = Seg n by A3, FUNCT_2:def 3;
then g is onto by A5, FUNCT_2:def 3;
hence Rev f in Permutations n by A3, MATRIX_1:def 12; :: thesis: verum