let n be Nat; :: thesis: for PERM being Permutation of (Permutations n)
for perm being Element of Permutations n st not perm is even & ( for p being Element of Permutations n holds PERM . p = p * perm ) holds
PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : not q is even }
set P = Permutations n;
let PERM be Permutation of (Permutations n); :: thesis: for perm being Element of Permutations n st not perm is even & ( for p being Element of Permutations n holds PERM . p = p * perm ) holds
PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : not q is even }
let perm be Element of Permutations n; :: thesis: ( not perm is even & ( for p being Element of Permutations n holds PERM . p = p * perm ) implies PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : not q is even } )
assume that
A1: not perm is even and
A2: for p being Element of Permutations n holds PERM . p = p * perm ; :: thesis: PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : not q is even }
set E = { p where p is Element of Permutations n : p is even } ;
set OD = { q where q is Element of Permutations n : not q is even } ;
for y being set holds
( y in { q where q is Element of Permutations n : not q is even } iff ex x being set st
( x in dom PERM & x in { p where p is Element of Permutations n : p is even } & y = PERM . x ) )

proof

let y be set ; :: thesis: ( y in { q where q is Element of Permutations n : not q is even } iff ex x being set st
( x in dom PERM & x in { p where p is Element of Permutations n : p is even } & y = PERM . x ) )
thus ( y in { q where q is Element of Permutations n : not q is even } implies ex x being set st
( x in dom PERM & x in { p where p is Element of Permutations n : p is even } & y = PERM . x ) ) :: thesis: ( ex x being set st
( x in dom PERM & x in { p where p is Element of Permutations n : p is even } & y = PERM . x ) implies y in { q where q is Element of Permutations n : not q is even } )

proof

reconsider perm9 = perm " as Element of Permutations n by MATRIX_7:18;
A3: dom PERM = Permutations n by FUNCT_2:67;
n >= 2 by A1, Lm3;
then A4: n >= 1 by XXREAL_0:2;
assume y in { q where q is Element of Permutations n : not q is even } ; :: thesis: ex x being set st
( x in dom PERM & x in { p where p is Element of Permutations n : p is even } & y = PERM . x )
then consider q being Element of Permutations n such that
A5: y = q and
A6: not q is even ;
A7: q * (idseq n) = q by MATRIX_2:24;
n is Element of NAT by ORDINAL1:def 13;
then not perm9 is even by A1, A4, MATRIX_7:28;
then A8: q * perm9 is even by A6, Th25;
reconsider qp9 = q * perm9 as Element of Permutations n by MATRIX_9:39;
take qp9 ; :: thesis: ( qp9 in dom PERM & qp9 in { p where p is Element of Permutations n : p is even } & y = PERM . qp9 )
A9: perm9 * perm = idseq n by MATRIX_2:25;
PERM . qp9 = qp9 * perm by A2;
hence ( qp9 in dom PERM & qp9 in { p where p is Element of Permutations n : p is even } & y = PERM . qp9 ) by A5, A3, A9, A7, A8, RELAT_1:55; :: thesis: verum

end;

assume ex x being set st
( x in dom PERM & x in { p where p is Element of Permutations n : p is even } & y = PERM . x ) ; :: thesis: y in { q where q is Element of Permutations n : not q is even }
then consider x being set such that
x in dom PERM and
A10: x in { p where p is Element of Permutations n : p is even } and
A11: y = PERM . x ;
consider p being Element of Permutations n such that
A12: p = x and
A13: p is even by A10;
reconsider pp = p * perm as Element of Permutations n by MATRIX_9:39;
A14: PERM . x = p * perm by A2, A12;
not pp is even by A1, A13, Th25;
hence y in { q where q is Element of Permutations n : not q is even } by A11, A14; :: thesis: verum

end;

hence PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : not q is even } by FUNCT_1:def 12; :: thesis: verum