let n be Nat; :: thesis: ( n >= 2 implies ex ODD, EVEN being finite set st
( EVEN = { p where p is Element of Permutations n : p is even } & ODD = { q where q is Element of Permutations n : q is odd } & EVEN /\ ODD = {} & EVEN \/ ODD = Permutations n & card EVEN = card ODD ) )
assume A1: n >= 2 ; :: thesis: ex ODD, EVEN being finite set st
( EVEN = { p where p is Element of Permutations n : p is even } & ODD = { q where q is Element of Permutations n : q is odd } & EVEN /\ ODD = {} & EVEN \/ ODD = Permutations n & card EVEN = card ODD )
1 <= n by A1, XXREAL_0:2;
then A2: 1 in Seg n ;
2 in Seg n by A1;
then consider O, E being finite set such that
A3: ( E = { p where p is Element of Permutations n : p is even } & O = { q where q is Element of Permutations n : q is odd } ) and
A4: ( E /\ O = {} & E \/ O = Permutations n ) and
A5: ex P being Function of E,O ex perm being Element of Permutations n st
( perm is being_transposition & perm . 1 = 2 & dom P = E & P is bijective & ( for p being Element of Permutations n st p in E holds
P . p = p * perm ) ) by A2, Lm8;
consider P being Function of E,O, perm being Element of Permutations n such that
perm is being_transposition and
perm . 1 = 2 and
A6: dom P = E and
A7: P is bijective and
for p being Element of Permutations n st p in E holds
P . p = p * perm by A5;
rng P = O by A7, FUNCT_2:def 3;
then E,O are_equipotent by A6, A7, WELLORD2:def 4;
then card E = card O by CARD_1:5;
hence ex ODD, EVEN being finite set st
( EVEN = { p where p is Element of Permutations n : p is even } & ODD = { q where q is Element of Permutations n : q is odd } & EVEN /\ ODD = {} & EVEN \/ ODD = Permutations n & card EVEN = card ODD ) by A3, A4; :: thesis: verum