environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FINSET_1, FINSEQ_1, RELAT_1, TARSKI, RPR_1, NAT_1, CARD_1, SUBSET_1, FUNCT_1, REAL_1, ARYTM_3, UPROOTS, SETFAM_1, MATRPROB, VALUED_1, CARD_3, PROB_2, XXREAL_0, ORDINAL4, PARTFUN1, DIST_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, CARD_1, CARD_3, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_2, VALUED_1, FUNCT_2, SETFAM_1, RPR_1, PROB_2, RVSUM_1, UPROOTS, MATRPROB;
definitions TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, FINSEQ_2, CARD_2, FINSEQ_4, FUNCT_1, FINSEQ_1, XBOOLE_0, XXREAL_0, PROB_2, NAT_1, RELAT_1, ZFMISC_1, FUNCT_2, XCMPLX_1, VALUED_1, FINSEQ_5, CARD_1, RVSUM_1, MATRPROB, XREAL_0, RELSET_1;
schemes NAT_1, FINSEQ_1, FUNCT_2, SUBSET_1, CLASSES1;
registrations FUNCT_1, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, ORDINAL1, FINSEQ_1, RELAT_1, FINSET_1, NUMBERS, VALUED_0, VALUED_1, CARD_1, MATRPROB, ENTROPY1;
constructors HIDDEN, RPR_1, RVSUM_1, BINOP_2, PARTFUN3, PROB_2, UPROOTS, MATRPROB, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities RPR_1, FINSEQ_1, RELAT_1, CARD_3, XBOOLE_0;
expansions TARSKI, FUNCT_1, XBOOLE_0;
Lm1:
for S being Function
for X being set st S is disjoint_valued holds
S | X is disjoint_valued
Lm2:
for n being Nat
for S being Function
for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & n = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
Lm3:
for S being finite set
for s being FinSequence of S st s in Finseq-EQclass (canFS S) holds
s is uniformly_distributed
by Th5, Th20;
Lm4:
for S being finite set
for s being FinSequence of S st s is uniformly_distributed holds
for t being FinSequence of S st t is uniformly_distributed holds
t in Finseq-EQclass s