let n be Nat; for A being object holds Election (A,n,A,0) = {(n |-> A)}
let A be object ; Election (A,n,A,0) = {(n |-> A)}
A1:
{A,A} = {A}
by ENUMSET1:29;
thus
Election (A,n,A,0) c= {(n |-> A)}
XBOOLE_0:def 10 {(n |-> A)} c= Election (A,n,A,0)
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; verum