environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, MESFUNC8, SEQFUNC, MESFUNC5, SUBSET_1, SUPINF_1, NAT_1, FUNCT_1, XXREAL_0, ORDINAL2, RELAT_1, XXREAL_2, RINFSUP1, ARYTM_3, PBOOLE, PARTFUN1, PROB_1, MEASURE1, CARD_1, SUPINF_2, MESFUNC1, VALUED_0, SEQ_2, ARYTM_1, TARSKI, REAL_1, INTEGRA5, VALUED_1, COMPLEX1, RFUNCT_3, MESFUNC2, MESFUN10;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, EXTREAL1, XCMPLX_0, XREAL_0, REAL_1, XXREAL_0, XXREAL_2, RELAT_1, FUNCT_1, RELSET_1, DOMAIN_1, NAT_1, VALUED_0, FUNCT_2, PARTFUN1, PROB_1, SUPINF_1, SUPINF_2, MEASURE1, MESFUNC1, MEASURE6, MESFUNC2, SEQFUNC, MESFUNC5, MESFUNC8, RINFSUP2;
definitions ;
theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, MESFUNC1, XREAL_0, XBOOLE_0, XBOOLE_1, MESFUNC2, XREAL_1, XXREAL_0, MESFUNC5, NAT_1, RELAT_1, FUNCT_2, SEQFUNC, ORDINAL1, MESFUNC8, RINFSUP2, MESFUNC7, MESFUNC9, NUMBERS, XXREAL_2, XXREAL_3;
schemes FUNCT_2, SEQFUNC, FUNCT_1;
registrations NAT_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, XBOOLE_0, SUPINF_2, NUMBERS, XXREAL_0, MESFUNC8, RINFSUP2, VALUED_0, MEMBER_1, RELSET_1, FUNCT_2;
constructors HIDDEN, REAL_1, DOMAIN_1, EXTREAL1, MESFUNC1, MEASURE6, MESFUNC2, MESFUNC5, RINFSUP2, MESFUNC9, SUPINF_1, MESFUNC8, SEQFUNC, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities MESFUNC1, RINFSUP2, XXREAL_3, MEMBER_1, SUPINF_2;
expansions ;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm1:
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )