theorem Th10: :: BALLOT_1:11

for n, k being Nat
for A, B being object holds Election (A,n,B,k) = Choose ((Seg (n + k)),n,A,B)