theorem :: BALLOT_1:25

for n, k being Nat holds card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k))