set BALL = { v where v is Element of (n + k) -tuples_on {A,B} : v is A,n,B,k -dominated-election } ;
{ v where v is Element of (n + k) -tuples_on {A,B} : v is A,n,B,k -dominated-election } c= Election (A,n,B,k)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (n + k) -tuples_on {A,B} : v is A,n,B,k -dominated-election } or x in Election (A,n,B,k) )
assume x in { v where v is Element of (n + k) -tuples_on {A,B} : v is A,n,B,k -dominated-election } ; :: thesis: x in Election (A,n,B,k)
then ex v being Element of (n + k) -tuples_on {A,B} st
( x = v & v is A,n,B,k -dominated-election ) ;
hence x in Election (A,n,B,k) ; :: thesis: verum

end;

then reconsider BALL = { v where v is Element of (n + k) -tuples_on {A,B} : v is A,n,B,k -dominated-election } as Subset of (Election (A,n,B,k)) ;
take BALL ; :: thesis: for f being FinSequence holds
( f in BALL iff f is A,n,B,k -dominated-election )
let f be FinSequence; :: thesis: ( f in BALL iff f is A,n,B,k -dominated-election )
( f in BALL implies f is A,n,B,k -dominated-election )

proof

assume f in BALL ; :: thesis: f is A,n,B,k -dominated-election
then ex v being Element of (n + k) -tuples_on {A,B} st
( f = v & v is A,n,B,k -dominated-election ) ;
hence f is A,n,B,k -dominated-election ; :: thesis: verum

end;

hence ( f in BALL iff f is A,n,B,k -dominated-election ) ; :: thesis: verum