let n, k be Nat; :: thesis: for A, B being object
for v being Element of (n + k) -tuples_on {A,B} st A <> B holds
( v in Election (A,n,B,k) iff card (v " {B}) = k )
let A, B be object ; :: thesis: for v being Element of (n + k) -tuples_on {A,B} st A <> B holds
( v in Election (A,n,B,k) iff card (v " {B}) = k )
let v be Element of (n + k) -tuples_on {A,B}; :: thesis: ( A <> B implies ( v in Election (A,n,B,k) iff card (v " {B}) = k ) )
assume A1: A <> B ; :: thesis: ( v in Election (A,n,B,k) iff card (v " {B}) = k )
A2: rng v c= {A,B} ;
A3: len v = n + k by CARD_1:def 7;
A4: (card (v " {A})) + (card (v " {B})) = len v by Th6, A2, A1;
thus ( v in Election (A,n,B,k) implies card (v " {B}) = k ) :: thesis: ( card (v " {B}) = k implies v in Election (A,n,B,k) )

proof

assume v in Election (A,n,B,k) ; :: thesis: card (v " {B}) = k
then card (v " {A}) = n by Def1;
hence card (v " {B}) = k by A4, A3; :: thesis: verum

end;

assume card (v " {B}) = k ; :: thesis: v in Election (A,n,B,k)
hence v in Election (A,n,B,k) by A4, A3, Def1; :: thesis: verum