environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, PROB_1, XBOOLE_0, TARSKI, FUNCT_1, RELAT_1, NAT_1, PROB_2, FUNCOP_1, FUNCT_7, CARD_1, XXREAL_0, ARYTM_3, ZFMISC_1, CARD_3, EQREL_1, RPR_1, ARYTM_1, SERIES_1, SEQ_2, ORDINAL2, PROB_3, SUPINF_2, REAL_1, XXREAL_2, SUPINF_1, MEASURE1, VALUED_0, SETFAM_1, MEASURE3, PROB_4, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, XREAL_0, CARD_3, ORDINAL1, MEASURE3, SUPINF_2, XXREAL_0, XXREAL_2, XCMPLX_0, NAT_1, SEQ_2, SETFAM_1, FUNCT_1, RELSET_1, SUBSET_1, NUMBERS, SUPINF_1, PARTFUN1, FUNCT_2, FUNCT_7, PROB_1, PROB_3, MEASURE1, FUNCOP_1, SEQM_3, SERIES_1, RINFSUP1, ZFMISC_1, MEASURE6, PROB_2;
definitions TARSKI, XBOOLE_0, PROB_3;
theorems FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, XREAL_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, PROB_2, RINFSUP1, SUPINF_2, SEQM_3, CARD_3, SETLIM_1, PROB_1, SERIES_1, PROB_3, MEASURE1, MEASURE3, ZFMISC_1, XXREAL_0, ORDINAL1, NUMBERS, XXREAL_2, FUNCT_7, DYNKIN, VALUED_0, FUNCOP_1, RELAT_1, XREAL_0;
schemes FUNCT_2, NAT_1, XFAMILY;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, NAT_1, MEMBERED, MEASURE1, MEASURE3, VALUED_0, SEQ_2, SEQ_4, FUNCT_7, PROB_1, RELSET_1, PROB_3;
constructors HIDDEN, REAL_1, SERIES_1, MEASURE3, MEASURE6, PARTFUN3, KURATO_0, RINFSUP1, PROB_3, SUPINF_1, FUNCT_7, RELSET_1, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, SERIES_1, SUBSET_1, SUPINF_2;
expansions TARSKI, XBOOLE_0, SERIES_1, PROB_3, FUNCT_2;
Lm1:
for A, B, C being set st C c= B holds
A \ C = (A \ B) \/ (A /\ (B \ C))
Lm2:
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Nat holds (Partial_Union A1) . n = A1 . n