let n, k, i, j be Nat; :: thesis: for A, B being object
for f, g being FinSequence st f is A,n,B,k -dominated-election & g is A,i,B,j -dominated-election holds
f ^ g is A,n + i,B,k + j -dominated-election
let A, B be object ; :: thesis: for f, g being FinSequence st f is A,n,B,k -dominated-election & g is A,i,B,j -dominated-election holds
f ^ g is A,n + i,B,k + j -dominated-election
let f, g be FinSequence; :: thesis: ( f is A,n,B,k -dominated-election & g is A,i,B,j -dominated-election implies f ^ g is A,n + i,B,k + j -dominated-election )
assume that
A1: f is A,n,B,k -dominated-election and
A2: g is A,i,B,j -dominated-election ; :: thesis: f ^ g is A,n + i,B,k + j -dominated-election
A3: A <> B by A1, Th13;
reconsider F = f as Element of (n + k) -tuples_on {A,B} by A1;
reconsider G = g as Element of (i + j) -tuples_on {A,B} by A2;
A4: len F = n + k by CARD_1:def 7;
A5: len (F ^ G) = (n + k) + (i + j) by CARD_1:def 7;
then reconsider FG = F ^ G as Element of ((n + k) + (i + j)) -tuples_on {A,B} by FINSEQ_2:92;
card (FG " {A}) = (card (F " {A})) + (card (G " {A})) by FINSEQ_3:57
.= n + (card (G " {A})) by A1, Def1
.= n + i by A2, Def1 ;
hence f ^ g in Election (A,(n + i),B,(k + j)) by Def1; :: according to BALLOT_1:def 2 :: thesis: for i being Nat st i > 0 holds
card (((f ^ g) | i) " {A}) > card (((f ^ g) | i) " {B})
let h be Nat; :: thesis: ( h > 0 implies card (((f ^ g) | h) " {A}) > card (((f ^ g) | h) " {B}) )
assume A6: h > 0 ; :: thesis: card (((f ^ g) | h) " {A}) > card (((f ^ g) | h) " {B})

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

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

then FG | h = F | h by A4, FINSEQ_5:22;
hence card (((f ^ g) | h) " {A}) > card (((f ^ g) | h) " {B}) by A1, A6; :: thesis: verum

end;

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

then reconsider h1 = h - (n + k) as Nat by NAT_1:21;
A8: h1 <> 0 by A7;
h1 + (len F) = h by A4;
then A9: FG | h = F ^ (G | h1) by FINSEQ_6:14;
then A10: card ((FG | h) " {A}) = (card (F " {A})) + (card ((G | h1) " {A})) by FINSEQ_3:57
.= n + (card ((G | h1) " {A})) by A1, Def1 ;
A11: card ((FG | h) " {B}) = (card (F " {B})) + (card ((G | h1) " {B})) by A9, FINSEQ_3:57
.= k + (card ((G | h1) " {B})) by A3, A1, Th11 ;
card ((G | h1) " {A}) > card ((G | h1) " {B}) by A8, A2;
hence card (((f ^ g) | h) " {A}) > card (((f ^ g) | h) " {B}) by A10, A11, Th14, A1, XREAL_1:8; :: thesis: verum

end;

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

then A12: FG | h = FG by FINSEQ_1:58, A5;
A13: card (FG " {A}) = (card (F " {A})) + (card (G " {A})) by FINSEQ_3:57
.= n + (card (G " {A})) by A1, Def1
.= n + i by A2, Def1 ;
A14: card (FG " {B}) = (card (F " {B})) + (card (G " {B})) by FINSEQ_3:57
.= k + (card (G " {B})) by A3, A1, Th11
.= k + j by A3, A2, Th11 ;
n > k by Th14, A1;
hence card (((f ^ g) | h) " {A}) > card (((f ^ g) | h) " {B}) by Th14, A2, A13, A14, XREAL_1:8, A12; :: thesis: verum

end;

end;