theorem Th22: :: BALLOT_1:22

for n, k being Nat
for p being FinSequence of NAT holds
( p is 0 ,n,1,k -dominated-election iff ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) )