let n, k be Nat; :: thesis: for A, B being object st A <> B holds
card (Election (A,n,B,k)) = (n + k) choose n
let A, B be object ; :: thesis: ( A <> B implies card (Election (A,n,B,k)) = (n + k) choose n )
assume A1: A <> B ; :: thesis: 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 ; :: thesis: verum