let n, k be Nat; :: thesis: 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 ; :: thesis: for f being FinSequence st f is A,n,B,k -dominated-election holds
A <> B
let f be FinSequence; :: thesis: ( f is A,n,B,k -dominated-election implies A <> B )
assume A1: f is A,n,B,k -dominated-election ; :: thesis: 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 ; :: thesis: verum