let n, k be Nat; :: thesis: for A, B being object holds Election (A,n,B,k) = Choose ((Seg (n + k)),n,A,B)
let A, B be object ; :: thesis: Election (A,n,B,k) = Choose ((Seg (n + k)),n,A,B)
thus Election (A,n,B,k) c= Choose ((Seg (n + k)),n,A,B) :: according to XBOOLE_0:def 10 :: thesis: Choose ((Seg (n + k)),n,A,B) c= Election (A,n,B,k)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Election (A,n,B,k) or x in Choose ((Seg (n + k)),n,A,B) )
assume A1: x in Election (A,n,B,k) ; :: thesis: x in Choose ((Seg (n + k)),n,A,B)
then reconsider v = x as Element of (n + k) -tuples_on {A,B} ;
A2: rng v c= {A,B} ;
len v = n + k by CARD_1:def 7;
then dom v = Seg (n + k) by FINSEQ_1:def 3;
then reconsider V = v as Function of (Seg (n + k)),{A,B} by FUNCT_2:2, A2;
card (v " {A}) = n by A1, Def1;
then V in Choose ((Seg (n + k)),n,A,B) by CARD_FIN:def 1;
hence x in Choose ((Seg (n + k)),n,A,B) ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Choose ((Seg (n + k)),n,A,B) or x in Election (A,n,B,k) )
assume x in Choose ((Seg (n + k)),n,A,B) ; :: thesis: x in Election (A,n,B,k)
then consider f being Function of (Seg (n + k)),{A,B} such that
A3: f = x and
A4: card (f " {A}) = n by CARD_FIN:def 1;
A5: rng f c= {A,B} ;
A6: dom f = Seg (n + k) by FUNCT_2:def 1;
then reconsider f = f as FinSequence by FINSEQ_1:def 2;
reconsider f = f as FinSequence of {A,B} by A5, FINSEQ_1:def 4;
n + k in NAT by ORDINAL1:def 12;
then len f = n + k by FINSEQ_1:def 3, A6;
then f is Element of (n + k) -tuples_on {A,B} by FINSEQ_2:92;
hence x in Election (A,n,B,k) by A3, A4, Def1; :: thesis: verum