environ
vocabularies HIDDEN, NUMBERS, NAT_1, FUNCT_1, ZFMISC_1, FINSEQ_1, RELAT_1, CARD_3, ARYTM_3, SUBSET_1, XXREAL_0, TARSKI, XBOOLE_0, FINSEQ_2, ARYTM_1, PARTFUN1, BINOP_2, ORDINAL4, CARD_1, FUNCOP_1, PROB_1, MESFUNC2, FUNCT_3, SUPINF_2, PROB_2, MEASURE1, XXREAL_2, ORDINAL2, SUPINF_1, XREAL_0, MESFUNC1, VALUED_0, COMPLEX1, SETFAM_1, FINSET_1, FINSOP_1, INTEGRA1, REAL_1, MESFUNC3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XREAL_0, FINSEQ_1, SETFAM_1, FUNCOP_1, FINSOP_1, FUNCT_3, FINSET_1, PROB_1, PROB_2, XXREAL_0, XXREAL_2, XXREAL_3, NAT_1, REAL_1, XCMPLX_0, SUPINF_1, SUPINF_2, MEASURE1, FINSEQOP, FINSEQ_2, BINOP_1, BINOP_2, RVSUM_1, EXTREAL1, MESFUNC1, MESFUNC2;
definitions TARSKI, XBOOLE_0;
theorems MEASURE1, TARSKI, FUNCT_1, FUNCT_2, NAT_1, SUPINF_2, EXTREAL1, ZFMISC_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCOP_1, FINSEQ_4, PROB_2, FUNCT_3, XBOOLE_0, XBOOLE_1, RELAT_1, RVSUM_1, MESFUNC2, MEASURE2, CARD_2, XREAL_1, XXREAL_0, ORDINAL1, NUMBERS, VALUED_1, XXREAL_2, VALUED_0, XXREAL_3, XREAL_0;
schemes FINSEQ_1, FINSEQ_2, NAT_1, PARTFUN1, BINOP_1;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, MEASURE1, FINSET_1, VALUED_0, CARD_1, CARD_3, XXREAL_3, RELSET_1;
constructors HIDDEN, PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, FINSEQOP, PROB_2, FINSOP_1, RVSUM_1, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, BINARITH, MESFUNC2, BINOP_2, SUPINF_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, BINOP_1, SUPINF_2, MESFUNC1;
expansions TARSKI, XBOOLE_0;
Lm1:
for a being FinSequence of ExtREAL
for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p
Lm2:
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & ( for x being object st x in dom f holds
0. <> f . x ) holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )
Lm3:
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & ex x being set st
( x in dom f & 0. = f . x ) holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )