let n be Nat; :: thesis: for A, B being object st A <> B & n > 0 holds
n |-> A is A,n,B, 0 -dominated-election
let A, B be object ; :: thesis: ( A <> B & n > 0 implies n |-> A is A,n,B, 0 -dominated-election )
set nA = n |-> A;
assume that
A1: A <> B and
A2: n > 0 ; :: thesis: n |-> A is A,n,B, 0 -dominated-election
A is Element of {A,B} by TARSKI:def 2;
then reconsider nA = n |-> A as Element of (n + 0) -tuples_on {A,B} by FINSEQ_2:112;
nA " (rng nA) c= nA " {A} by FUNCOP_1:13, RELAT_1:143;
then dom nA = nA " {A} by RELAT_1:132, RELAT_1:134;
then card (nA " {A}) = card (Seg (len nA)) by FINSEQ_1:def 3
.= len nA by FINSEQ_1:57
.= n by CARD_1:def 7 ;
hence n |-> A in Election (A,n,B,0) by Def1; :: according to BALLOT_1:def 2 :: thesis: for i being Nat st i > 0 holds
card (((n |-> A) | i) " {A}) > card (((n |-> A) | i) " {B})
let i be Nat; :: thesis: ( i > 0 implies card (((n |-> A) | i) " {A}) > card (((n |-> A) | i) " {B}) )
assume A3: i > 0 ; :: thesis: card (((n |-> A) | i) " {A}) > card (((n |-> A) | i) " {B})
set nAi = nA | i;
A4: nA | i = ((Seg n) /\ (Seg i)) --> A by FUNCOP_1:12;
A5: not A in {B} by A1, TARSKI:def 1;

per cases ( i <= n or i > n ) ;

suppose i <= n ; :: thesis: card (((n |-> A) | i) " {A}) > card (((n |-> A) | i) " {B})

then (Seg i) /\ (Seg n) = Seg i by FINSEQ_1:5, XBOOLE_1:28;
then A6: (nA | i) " {A} = Seg i by A4, FUNCOP_1:15;
(nA | i) " {B} = {} by A5, FUNCOP_1:16, A4;
hence card (((n |-> A) | i) " {A}) > card (((n |-> A) | i) " {B}) by A6, A3; :: thesis: verum

end;

suppose i > n ; :: thesis: card (((n |-> A) | i) " {A}) > card (((n |-> A) | i) " {B})

then (Seg i) /\ (Seg n) = Seg n by FINSEQ_1:5, XBOOLE_1:28;
then A7: (nA | i) " {A} = Seg n by A4, FUNCOP_1:15;
(nA | i) " {B} = {} by A5, FUNCOP_1:16, A4;
hence card (((n |-> A) | i) " {A}) > card (((n |-> A) | i) " {B}) by A2, A7; :: thesis: verum

end;

end;