let n be Nat; :: thesis: for PERM being Permutation of (Permutations n)
for perm being Element of Permutations n st perm is odd & ( 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 : q is odd }
set P = Permutations n;
let PERM be Permutation of (Permutations n); :: thesis: for perm being Element of Permutations n st perm is odd & ( 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 : q is odd }
let perm be Element of Permutations n; :: thesis: ( perm is odd & ( 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 : q is odd } )
assume that
A1: perm is odd 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 : q is odd }
set E = { p where p is Element of Permutations n : p is even } ;
set OD = { q where q is Element of Permutations n : q is odd } ;
for y being object holds
( y in { q where q is Element of Permutations n : q is odd } iff ex x being object 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 object ; :: thesis: ( y in { q where q is Element of Permutations n : q is odd } iff ex x being object 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 : q is odd } implies ex x being object 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 object 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 : q is odd } )

proof

reconsider perm9 = perm " as Element of Permutations n by MATRIX_7:18;
A3: dom PERM = Permutations n by FUNCT_2:52;
n >= 2 by A1, Lm3;
then A4: n >= 1 by XXREAL_0:2;
assume y in { q where q is Element of Permutations n : q is odd } ; :: thesis: ex x being object 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: q is odd ;
A7: q * (idseq n) = q by MATRIX_1:12;
perm9 is odd 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_1:13;
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:36; :: thesis: verum

end;

given x being object 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 ; :: thesis: y in { q where q is Element of Permutations n : q is odd }
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;
pp is odd by A1, A13, Th25;
hence y in { q where q is Element of Permutations n : q is odd } 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 : q is odd } by FUNCT_1:def 6; :: thesis: verum