let n, k be Nat; for A, B being object st A <> B holds
card (Election (A,n,B,k)) = (n + k) choose n
let A, B be object ; ( A <> B implies card (Election (A,n,B,k)) = (n + k) choose n )
assume A1:
A <> B
; card (Election (A,n,B,k)) = (n + k) choose n
thus card (Election (A,n,B,k)) =
card (Choose ((Seg (n + k)),n,A,B))
by Th10
.=
(card (Seg (n + k))) choose n
by A1, CARD_FIN:16
.=
(n + k) choose n
by FINSEQ_1:57
; verum