let n be Nat; :: thesis: card { p where p is odd-valued a_partition of n : verum } = card { p where p is one-to-one a_partition of n : verum }
set OddVall = { p where p is odd-valued a_partition of n : verum } ;
set OneToOne = { p where p is one-to-one a_partition of n : verum } ;
A1: the odd-valued a_partition of n in { p where p is odd-valued a_partition of n : verum } ;
ex E being Function of { p where p is one-to-one a_partition of n : verum } , { p where p is odd-valued a_partition of n : verum } st
for p being one-to-one a_partition of n holds E . p = Euler_transformation p
proof
defpred S1[ object , object ] means for p being one-to-one a_partition of n st p = $1 holds
$2 = Euler_transformation p;
A2: for x being object st x in { p where p is one-to-one a_partition of n : verum } holds
ex y being object st
( y in { p where p is odd-valued a_partition of n : verum } & S1[x,y] )
proof
let x be object ; :: thesis: ( x in { p where p is one-to-one a_partition of n : verum } implies ex y being object st
( y in { p where p is odd-valued a_partition of n : verum } & S1[x,y] ) )
assume x in { p where p is one-to-one a_partition of n : verum } ; :: thesis: ex y being object st
( y in { p where p is odd-valued a_partition of n : verum } & S1[x,y] )
then ex q being one-to-one a_partition of n st x = q ;
then reconsider x = x as one-to-one a_partition of n ;
take Euler_transformation x ; :: thesis: ( Euler_transformation x in { p where p is odd-valued a_partition of n : verum } & S1[x, Euler_transformation x] )
thus ( Euler_transformation x in { p where p is odd-valued a_partition of n : verum } & S1[x, Euler_transformation x] ) ; :: thesis: verum
end;
consider f being Function of { p where p is one-to-one a_partition of n : verum } , { p where p is odd-valued a_partition of n : verum } such that
A3: for x being object st x in { p where p is one-to-one a_partition of n : verum } holds
S1[x,f . x] from FUNCT_2:sch 1(A2);
 take f ; :: thesis: for p being one-to-one a_partition of n holds f . p = Euler_transformation p
let p be one-to-one a_partition of n; :: thesis: f . p = Euler_transformation p
p in { p where p is one-to-one a_partition of n : verum } ;
hence f . p = Euler_transformation p by A3; :: thesis: verum
end;
then consider E being Function of { p where p is one-to-one a_partition of n : verum } , { p where p is odd-valued a_partition of n : verum } such that
A4: for p being one-to-one a_partition of n holds E . p = Euler_transformation p ;
A5: dom E = { p where p is one-to-one a_partition of n : verum } by A1, FUNCT_2:def 1;
{ p where p is odd-valued a_partition of n : verum } c= rng E
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { p where p is odd-valued a_partition of n : verum } or p in rng E )
assume p in { p where p is odd-valued a_partition of n : verum } ; :: thesis: p in rng E
then ex o being odd-valued a_partition of n st o = p ;
then reconsider p = p as odd-valued a_partition of n ;
consider q being one-to-one a_partition of n such that
A6: p = Euler_transformation q by Th15;
( q in dom E & p = E . q ) by A6, A4, A5;
hence p in rng E by FUNCT_1:def 3; :: thesis: verum
end;
then A7: rng E = { p where p is odd-valued a_partition of n : verum } ;
E is one-to-one
proof
let p1, p2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not p1 in proj1 E or not p2 in proj1 E or not E . p1 = E . p2 or p1 = p2 )
assume A8: ( p1 in dom E & p2 in dom E & E . p1 = E . p2 ) ; :: thesis: p1 = p2
then ( ex o being one-to-one a_partition of n st o = p1 & ex o being one-to-one a_partition of n st o = p2 ) by A5;
then reconsider p1 = p1, p2 = p2 as one-to-one a_partition of n ;
( E . p1 = Euler_transformation p1 & E . p2 = Euler_transformation p2 ) by A4;
hence p1 = p2 by Th14, A8; :: thesis: verum
end;
hence card { p where p is odd-valued a_partition of n : verum } = card { p where p is one-to-one a_partition of n : verum } by A5, A7, CARD_1:70; :: thesis: verum