let X be 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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
let F be 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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
let M be sigma_Measure of S; for E being Element of S st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
let E be Element of S; ( E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
assume that
A1:
E = dom (F . 0)
and
A2:
for n being Nat holds
( F . n is nonnegative & F . n is E -measurable )
and
A3:
for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x
and
A4:
Integral (M,((F . 0) | E)) < +infty
; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
A5:
F . 0 is nonnegative
by A2;
A6:
dom (F . 0) = dom |.(F . 0).|
by MESFUNC1:def 10;
A7:
for x being Element of X st x in dom (F . 0) holds
(F . 0) . x = |.(F . 0).| . x
A9:
F . 0 is E -measurable
by A2;
then
Integral (M,(F . 0)) = integral+ (M,(F . 0))
by A1, A5, MESFUNC5:88;
then
integral+ (M,(F . 0)) < +infty
by A1, A4, RELAT_1:68;
then A10:
integral+ (M,|.(F . 0).|) < +infty
by A6, A7, PARTFUN1:5;
A11:
max+ (F . 0) is E -measurable
by A2, MESFUNC2:25;
for x being object st x in dom (max- (F . 0)) holds
0. <= (max- (F . 0)) . x
by MESFUNC2:13;
then A12:
max- (F . 0) is nonnegative
by SUPINF_2:52;
A13:
for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= (F . 0) . x
A16:
for x being Element of X st x in E holds
F # x is convergent
A18:
dom (max+ (F . 0)) = dom (F . 0)
by MESFUNC2:def 2;
then A19:
(max+ (F . 0)) | E = max+ (F . 0)
by A1, RELAT_1:68;
for x being object st x in dom (max+ (F . 0)) holds
0. <= (max+ (F . 0)) . x
by MESFUNC2:12;
then A20:
max+ (F . 0) is nonnegative
by SUPINF_2:52;
then A21:
dom ((max+ (F . 0)) + (max- (F . 0))) = (dom (max+ (F . 0))) /\ (dom (max- (F . 0)))
by A12, MESFUNC5:22;
A22:
dom (max- (F . 0)) = dom (F . 0)
by MESFUNC2:def 3;
then A23:
(max- (F . 0)) | E = max- (F . 0)
by A1, RELAT_1:68;
max- (F . 0) is E -measurable
by A1, A2, MESFUNC2:26;
then
ex C being Element of S st
( C = dom ((max+ (F . 0)) + (max- (F . 0))) & integral+ (M,((max+ (F . 0)) + (max- (F . 0)))) = (integral+ (M,((max+ (F . 0)) | C))) + (integral+ (M,((max- (F . 0)) | C))) )
by A1, A18, A22, A20, A12, A11, MESFUNC5:78;
then A24:
(integral+ (M,(max+ (F . 0)))) + (integral+ (M,(max- (F . 0)))) < +infty
by A1, A18, A22, A21, A19, A23, A10, MESFUNC2:24;
0 <= integral+ (M,(max- (F . 0)))
by A1, A9, A22, A12, MESFUNC2:26, MESFUNC5:79;
then
integral+ (M,(max+ (F . 0))) <> +infty
by A24, XXREAL_3:def 2;
then A25:
integral+ (M,(max+ (F . 0))) < +infty
by XXREAL_0:4;
0 <= integral+ (M,(max+ (F . 0)))
by A1, A9, A18, A20, MESFUNC2:25, MESFUNC5:79;
then
integral+ (M,(max- (F . 0))) <> +infty
by A24, XXREAL_3:def 2;
then
integral+ (M,(max- (F . 0))) < +infty
by XXREAL_0:4;
then
F . 0 is_integrable_on M
by A1, A9, A25;
then
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)) ) ) )
by A1, A2, A13, Th17;
hence
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
by A16; verum