let n, k, i be Nat; :: thesis: 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
let A, B be object ; :: thesis: 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
let f be FinSequence; :: thesis: ( f is A,n,B,k -dominated-election & i < n - k implies f ^ (i |-> B) is A,n,B,k + i -dominated-election )
set iB = i |-> B;
assume that
A1: f is A,n,B,k -dominated-election and
A2: i < n - k ; :: thesis: f ^ (i |-> B) is A,n,B,k + i -dominated-election
A3: A <> B by A1, Th13;
A4: rng (i |-> B) c= {B} by FUNCOP_1:13;
{B} c= {A,B} by ZFMISC_1:7;
then rng (i |-> B) c= {A,B} by A4;
then reconsider iB = i |-> B as FinSequence of {A,B} by FINSEQ_1:def 4;
reconsider F = f as Element of (n + k) -tuples_on {A,B} by A1;
set fB = f ^ (i |-> B);
A5: len f = n + k by A1, CARD_1:def 7;
A6: len (F ^ iB) = (n + k) + i by CARD_1:def 7;
then reconsider FB = F ^ iB as Element of (n + (k + i)) -tuples_on {A,B} by FINSEQ_2:92;
A7: not B in {A} by A3, TARSKI:def 1;
then A8: iB " {A} = {} by FUNCOP_1:16;
A9: card (FB " {A}) = (card (F " {A})) + (card (iB " {A})) by FINSEQ_3:57;
A10: card (F " {A}) = n by Def1, A1;
hence f ^ (i |-> B) in Election (A,n,B,(k + i)) by A9, A8, Def1; :: according to BALLOT_1:def 2 :: thesis: for i being Nat st i > 0 holds
card (((f ^ (i |-> B)) | i) " {A}) > card (((f ^ (i |-> B)) | i) " {B})
let j be Nat; :: thesis: ( j > 0 implies card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B}) )
assume A11: j > 0 ; :: thesis: card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B})
set FBj = FB | j;
A12: card (f " {B}) = k by A3, Th11, A1;
A13: i + k < (n - k) + k by A2, XREAL_1:6;

per cases ( j <= n + k or ( j > n + k & j <= (n + k) + i ) or j > (n + k) + i ) ;

suppose j <= n + k ; :: thesis: card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B})

then FB | j = f | j by A5, FINSEQ_5:22;
hence card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B}) by A11, A1; :: thesis: verum

end;

suppose A14: ( j > n + k & j <= (n + k) + i ) ; :: thesis: card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B})

then reconsider j1 = j - (n + k) as Nat by NAT_1:21;
A15: j1 + (n + k) <= i + (n + k) by A14;
then A16: j1 <= i by XREAL_1:6;
(Seg i) /\ (Seg j1) = Seg j1 by A15, XREAL_1:6, FINSEQ_1:7;
then A17: iB | (Seg j1) = (Seg j1) --> B by FUNCOP_1:12;
A18: ((Seg j1) --> B) " {A} = {} by A7, FUNCOP_1:16;
A19: FB | j = FB | (Seg ((len F) + j1)) by A5
.= F ^ ((Seg j1) --> B) by A17, FINSEQ_6:14 ;
then A20: card ((FB | j) " {A}) = n + (card (((Seg j1) --> B) " {A})) by A10, FINSEQ_3:57
.= n by A18 ;
B in {B} by TARSKI:def 1;
then ((Seg j1) --> B) " {B} = Seg j1 by FUNCOP_1:14;
then card ((FB | j) " {B}) = k + (card (Seg j1)) by A12, A19, FINSEQ_3:57
.= k + j1 by FINSEQ_1:57 ;
then card ((FB | j) " {B}) <= k + i by A16, XREAL_1:6;
hence card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B}) by A20, A13, XXREAL_0:2; :: thesis: verum

end;

suppose j > (n + k) + i ; :: thesis: card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B})

then A21: FB | j = FB by FINSEQ_1:58, A6;
A22: iB " {A} = {} by A7, FUNCOP_1:16;
B in {B} by TARSKI:def 1;
then iB " {B} = Seg i by FUNCOP_1:14;
then card (FB " {B}) = k + (card (Seg i)) by A12, FINSEQ_3:57
.= k + i by FINSEQ_1:57 ;
hence card (((f ^ (i |-> B)) | j) " {A}) > card (((f ^ (i |-> B)) | j) " {B}) by A21, A22, A9, Def1, A1, A13; :: thesis: verum

end;

end;