let n be Nat; :: thesis: for A being object holds Election (A,n,A,0) = {(n |-> A)}
let A be object ; :: thesis: Election (A,n,A,0) = {(n |-> A)}
A1: {A,A} = {A} by ENUMSET1:29;
thus Election (A,n,A,0) c= {(n |-> A)} :: according to XBOOLE_0:def 10 :: thesis: {(n |-> A)} c= Election (A,n,A,0)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Election (A,n,A,0) or x in {(n |-> A)} )
assume A2: x in Election (A,n,A,0) ; :: thesis: x in {(n |-> A)}
then reconsider v = x as Element of (n + 0) -tuples_on {A} by ENUMSET1:29;
A3: card (v " {A}) = n by A2, Def1;
A4: len v = n by CARD_1:def 7;

per cases ( rng v = {} or rng v <> {} ) ;

suppose rng v = {} ; :: thesis: x in {(n |-> A)}

then v = {} --> {A} ;
then v = n |-> A by A3;
hence x in {(n |-> A)} by TARSKI:def 1; :: thesis: verum

end;

suppose rng v <> {} ; :: thesis: x in {(n |-> A)}

then v = (dom v) --> A by ZFMISC_1:33, FUNCOP_1:9;
then v = n |-> A by A4, FINSEQ_1:def 3;
hence x in {(n |-> A)} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

A in {A} by TARSKI:def 1;
then reconsider nA = n |-> A as Element of n -tuples_on {A,A} by A1, FINSEQ_2:112;
nA " {A} = Seg n by FUNCOP_1:15;
then card (nA " {A}) = n by FINSEQ_1:57;
then nA in Election (A,n,A,0) by Def1;
hence {(n |-> A)} c= Election (A,n,A,0) by ZFMISC_1:31; :: thesis: verum