environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, FINSET_1, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, FINSEQ_2, XXREAL_0, CARD_1, XBOOLE_0, ORDINAL4, CARD_3, FINSOP_1, FUNCOP_1, BINOP_2, REALSET1, FUNCT_4, CARD_FIN, BALLOT_1, RPR_1, REAL_1, PRGCOR_2, CATALAN2, VALUED_0, SETWISEO;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1, FUNCT_1, XCMPLX_0, FINSET_1, XXREAL_0, AFINSQ_1, RELSET_1, FINSEQ_1, FINSEQ_2, DOMAIN_1, FUNCT_2, FUNCT_4, FUNCOP_1, BINOP_2, AFINSQ_2, NEWTON, XREAL_0, RPR_1, CARD_FIN, CATALAN2, VALUED_0, FINSEQOP, SETWOP_2, RVSUM_1, NAT_D;
definitions TARSKI, XBOOLE_0, FUNCT_1;
theorems AFINSQ_1, TARSKI, FUNCT_1, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1, NAT_1, FUNCT_2, XCMPLX_1, CARD_2, WELLORD2, ENUMSET1, CARD_1, NEWTON, XREAL_1, FUNCOP_1, FUNCT_4, XXREAL_0, NAT_D, XREAL_0, AFINSQ_2, ORDINAL1, RPR_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, RVSUM_1, FINSEQ_3, FINSEQ_6, NECKLACE, CARD_FIN, CATALAN2;
schemes FUNCT_2, NAT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FUNCT_4, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, AFINSQ_1, RELSET_1, VALUED_0, AFINSQ_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, RVSUM_1;
constructors HIDDEN, PARTFUN3, BINOM, WELLORD2, SETWISEO, NAT_D, BINOP_2, RELSET_1, AFINSQ_2, RPR_1, CARD_FIN, CATALAN2, FINSEQOP, FINSOP_1, RVSUM_1, NEWTON;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FUNCOP_1, RELAT_1, ORDINAL1, FINSEQ_1, FINSEQ_2;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, CATALAN2;
theorem
for
n,
k,
i,
j being
Nat for
A,
B being
object for
f,
g being
FinSequence st
f is
A,
n,
B,
k -dominated-election &
g is
A,
i,
B,
j -dominated-election holds
f ^ g is
A,
n + i,
B,
k + j -dominated-election
definition
let A be
object ;
let n be
Nat;
let B be
object ;
let k be
Nat;
existence
ex b1 being Subset of (Election (A,n,B,k)) st
for f being FinSequence holds
( f in b1 iff f is A,n,B,k -dominated-election )
uniqueness
for b1, b2 being Subset of (Election (A,n,B,k)) st ( for f being FinSequence holds
( f in b1 iff f is A,n,B,k -dominated-election ) ) & ( for f being FinSequence holds
( f in b2 iff f is A,n,B,k -dominated-election ) ) holds
b1 = b2
end;