let n, k be Nat; :: thesis: card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k))
set D = Domin_0 ((n + k),k);
set B = DominatedElection (0,(n + 1),1,k);
set Z = <*0*>;
defpred S₁[ object , object ] means for d being XFinSequence of NAT st d = $1 holds
$2 = <*0*> ^ (XFS2FS d);
A1: for x being object st x in Domin_0 ((n + k),k) holds
ex y being object st
( y in DominatedElection (0,(n + 1),1,k) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Domin_0 ((n + k),k) implies ex y being object st
( y in DominatedElection (0,(n + 1),1,k) & S₁[x,y] ) )
assume A2: x in Domin_0 ((n + k),k) ; :: thesis: ex y being object st
( y in DominatedElection (0,(n + 1),1,k) & S₁[x,y] )
then consider p being XFinSequence of NAT such that
A3: p = x and
( p is dominated_by_0 & dom p = n + k & Sum p = k ) by CATALAN2:def 2;
take y = <*0*> ^ (XFS2FS p); :: thesis: ( y in DominatedElection (0,(n + 1),1,k) & S₁[x,y] )
thus ( y in DominatedElection (0,(n + 1),1,k) & S₁[x,y] ) by Th24, A3, A2; :: thesis: verum

end;

consider f being Function of (Domin_0 ((n + k),k)),(DominatedElection (0,(n + 1),1,k)) such that
A4: for x being object st x in Domin_0 ((n + k),k) holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);

per cases ( DominatedElection (0,(n + 1),1,k) <> {} or DominatedElection (0,(n + 1),1,k) = {} ) ;

suppose DominatedElection (0,(n + 1),1,k) <> {} ; :: thesis: card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k))

then A5: dom f = Domin_0 ((n + k),k) by FUNCT_2:def 1;
DominatedElection (0,(n + 1),1,k) c= rng f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in DominatedElection (0,(n + 1),1,k) or y in rng f )
assume A6: y in DominatedElection (0,(n + 1),1,k) ; :: thesis: y in rng f
then y in Election (0,(n + 1),1,k) ;
then reconsider g = y as Element of ((n + 1) + k) -tuples_on {0,1} ;
g is 0 ,n + 1,1,k -dominated-election by A6, Def3;
then A7: g . 1 = 0 by Th23;
consider d being Element of {0,1}, dg being FinSequence of {0,1} such that
A8: d = g . 1 and
A9: g = <*d*> ^ dg by FINSEQ_3:102;
{0,1} c= NAT ;
then rng (FS2XFS dg) c= NAT ;
then reconsider G = FS2XFS dg as XFinSequence of NAT by RELAT_1:def 19;
A10: XFS2FS G = dg ;
then A11: G in Domin_0 ((n + k),k) by A6, A8, A9, A7, Th24;
f . G = g by A10, A6, A8, A9, A7, Th24, A4;
hence y in rng f by A11, A5, FUNCT_1:def 3; :: thesis: verum

end;

then A12: rng f = DominatedElection (0,(n + 1),1,k) ;
f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A13: x1 in dom f and
A14: x2 in dom f and
A15: f . x1 = f . x2 ; :: thesis: x1 = x2
consider p1 being XFinSequence of NAT such that
A16: p1 = x1 and
( p1 is dominated_by_0 & dom p1 = n + k & Sum p1 = k ) by A13, CATALAN2:def 2;
consider p2 being XFinSequence of NAT such that
A17: p2 = x2 and
( p2 is dominated_by_0 & dom p2 = n + k & Sum p2 = k ) by A14, CATALAN2:def 2;
A18: f . p1 = <*0*> ^ (XFS2FS p1) by A16, A13, A4;
f . p2 = <*0*> ^ (XFS2FS p2) by A14, A17, A4;
then XFS2FS p1 = XFS2FS p2 by A18, A15, A16, A17, FINSEQ_1:33;
hence x1 = x2 by Th4, A16, A17; :: thesis: verum

end;

hence card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k)) by WELLORD2:def 4, A5, A12, CARD_1:5; :: thesis: verum

end;

suppose A19: DominatedElection (0,(n + 1),1,k) = {} ; :: thesis: card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k))

Domin_0 ((n + k),k) = {}

proof

assume Domin_0 ((n + k),k) <> {} ; :: thesis: contradiction
then consider x being object such that
A20: x in Domin_0 ((n + k),k) by XBOOLE_0:def 1;
ex y being object st
( y in DominatedElection (0,(n + 1),1,k) & S₁[x,y] ) by A20, A1;
hence contradiction by A19; :: thesis: verum

end;

hence card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k)) by A19; :: thesis: verum

end;

end;