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

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