let n, k be Nat; :: thesis: for A being object st k > 0 holds
Election (A,n,A,k) is empty
let A be object ; :: thesis: ( k > 0 implies Election (A,n,A,k) is empty )
assume A1: k > 0 ; :: thesis: Election (A,n,A,k) is empty
assume not Election (A,n,A,k) is empty ; :: thesis: contradiction
then consider v being object such that
A2: v in Election (A,n,A,k) ;
reconsider v = v as Element of (n + k) -tuples_on {A} by A2, ENUMSET1:29;
A3: card (dom v) = n + k by CARD_1:def 7;
v " (rng v) c= v " {A} by RELAT_1:143;
then v " {A} = dom v by RELAT_1:134, RELAT_1:132;
then n + k = n by A3, Def1, A2;
hence contradiction by A1; :: thesis: verum