theorem Th16: :: BALLOT_1:17

for n, k, i being Nat
for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election & i < n - k holds
f ^ (i |-> B) is A,n,B,k + i -dominated-election