let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

proof

let x be Element of X; :: thesis: ( x in dom (F . 0) implies (F . 0) . x = |.(F . 0).| . x )
0 <= (F . 0) . x by A5, SUPINF_2:51;
then A8: |.((F . 0) . x).| = (F . 0) . x by EXTREAL1:def 1;
assume x in dom (F . 0) ; :: thesis: (F . 0) . x = |.(F . 0).| . x
hence (F . 0) . x = |.(F . 0).| . x by A6, A8, MESFUNC1:def 10; :: thesis: verum

end;

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

proof

let x be Element of X; :: thesis: for n being Nat st x in E holds
|.(F . n).| . x <= (F . 0) . x
let n be Nat; :: thesis: ( x in E implies |.(F . n).| . x <= (F . 0) . x )
assume A14: x in E ; :: thesis: |.(F . n).| . x <= (F . 0) . x
F . n is nonnegative by A2;
then 0 <= (F . n) . x by SUPINF_2:51;
then |.((F . n) . x).| = (F . n) . x by EXTREAL1:def 1;
then A15: |.((F . n) . x).| <= (F . 0) . x by A3, A14;
dom (F . n) = dom |.(F . n).| by MESFUNC1:def 10;
then x in dom |.(F . n).| by A1, A14, MESFUNC8:def 2;
hence |.(F . n).| . x <= (F . 0) . x by A15, MESFUNC1:def 10; :: thesis: verum

end;

A16: for x being Element of X st x in E holds
F # x is convergent

proof

let x be Element of X; :: thesis: ( x in E implies F # x is convergent )
assume A17: x in E ; :: thesis: F # x is convergent

now :: thesis: for n, m being Nat st m <= n holds
(F # x) . n <= (F # x) . m

let n, m be Nat; :: thesis: ( m <= n implies (F # x) . n <= (F # x) . m )
assume m <= n ; :: thesis: (F # x) . n <= (F # x) . m
then (F . n) . x <= (F . m) . x by A3, A17;
then (F # x) . n <= (F . m) . x by MESFUNC5:def 13;
hence (F # x) . n <= (F # x) . m by MESFUNC5:def 13; :: thesis: verum

end;

then F # x is non-increasing by RINFSUP2:7;
hence F # x is convergent by RINFSUP2:36; :: thesis: verum

end;

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; :: thesis: verum