let n, k be Nat; for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election holds
A <> B
let A, B be object ; for f being FinSequence st f is A,n,B,k -dominated-election holds
A <> B
let f be FinSequence; ( f is A,n,B,k -dominated-election implies A <> B )
assume A1:
f is A,n,B,k -dominated-election
; A <> B
then reconsider f = f as Element of (n + k) -tuples_on {A,B} ;
(len f) + 1 >= len f
by NAT_1:13;
then
f | ((len f) + 1) = f
by FINSEQ_1:58;
then
card (f " {A}) > card (f " {B})
by A1;
hence
A <> B
; verum