let n, k, i, j be Nat; 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 ; 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; ( 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
; 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; BALLOT_1:def 2 for i being Nat st i > 0 holds
card (((f ^ g) | i) " {A}) > card (((f ^ g) | i) " {B})
let h be Nat; ( h > 0 implies card (((f ^ g) | h) " {A}) > card (((f ^ g) | h) " {B}) )
assume A6:
h > 0
; 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) + i) + j
;
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;
verum end; end;