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_measurable_on E ) ) & ( 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_measurable_on E ) ) & ( 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_measurable_on E ) ) & ( 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_measurable_on E ) ) & ( 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_measurable_on E ) ) & ( 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_measurable_on E ) 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 & F . 0 is_measurable_on E ) 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 )
assume A71: x in dom (F . 0 ) ; :: thesis: (F . 0 ) . x = |.(F . 0 ).| . x
0 <= (F . 0 ) . x by A5, SUPINF_2:70;
then |.((F . 0 ) . x).| = (F . 0 ) . x by EXTREAL1:def 3;
hence (F . 0 ) . x = |.(F . 0 ).| . x by A6, A71, MESFUNC1:def 10; :: thesis: verum

end;

A8: ( dom (max+ (F . 0 )) = dom (F . 0 ) & dom (max- (F . 0 )) = dom (F . 0 ) ) by MESFUNC2:def 2, MESFUNC2:def 3;
( ( for x being set st x in dom (max+ (F . 0 )) holds
0. <= (max+ (F . 0 )) . x ) & ( for x being set st x in dom (max- (F . 0 )) holds
0. <= (max- (F . 0 )) . x ) ) by MESFUNC2:14, MESFUNC2:15;
then A9: ( max+ (F . 0 ) is nonnegative & max- (F . 0 ) is nonnegative ) by SUPINF_2:71;
B1: dom ((max+ (F . 0 )) + (max- (F . 0 ))) = (dom (max+ (F . 0 ))) /\ (dom (max- (F . 0 ))) by A9, MESFUNC5:28;
B2: 0 <= integral+ M,(max+ (F . 0 )) by A1, A8, A5, A9, MESFUNC2:27, MESFUNC5:85;
B3: 0 <= integral+ M,(max- (F . 0 )) by A1, A8, A5, A9, MESFUNC2:28, MESFUNC5:85;
( max+ (F . 0 ) is_measurable_on E & max- (F . 0 ) is_measurable_on E ) by A1, A5, MESFUNC2:27, MESFUNC2:28;
then B4: 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, A8, A9, MESFUNC5:84;
B5: ( (max+ (F . 0 )) | E = max+ (F . 0 ) & (max- (F . 0 )) | E = max- (F . 0 ) ) by A1, A8, RELAT_1:97;
Integral M,(F . 0 ) = integral+ M,(F . 0 ) by A1, A5, MESFUNC5:94;
then integral+ M,(F . 0 ) < +infty by A4, A1, RELAT_1:97;
then integral+ M,|.(F . 0 ).| < +infty by A7, A6, PARTFUN1:34;
then (integral+ M,(max+ (F . 0 ))) + (integral+ M,(max- (F . 0 ))) < +infty by B5, B1, A1, A8, B4, MESFUNC2:26;
then ( integral+ M,(max+ (F . 0 )) <> +infty & integral+ M,(max- (F . 0 )) <> +infty ) by B2, B3, XXREAL_3:def 2;
then ( integral+ M,(max+ (F . 0 )) < +infty & integral+ M,(max- (F . 0 )) < +infty ) by XXREAL_0:4;
then C2: F . 0 is_integrable_on M by A1, A5, MESFUNC5:def 17;
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 C31: x in E ; :: thesis: |.(F . n).| . x <= (F . 0 ) . x
dom (F . n) = dom |.(F . n).| by MESFUNC1:def 10;
then C32: x in dom |.(F . n).| by C31, A1, MESFUNC8:def 2;
F . n is nonnegative by A2;
then 0 <= (F . n) . x by SUPINF_2:70;
then |.((F . n) . x).| = (F . n) . x by EXTREAL1:def 3;
then |.((F . n) . x).| <= (F . 0 ) . x by C31, A3;
hence |.(F . n).| . x <= (F . 0 ) . x by C32, MESFUNC1:def 10; :: thesis: verum

end;

then consider I being ExtREAL_sequence such that
C4: ( ( 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, A5, C2, Th136x;
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 C5: x in E ; :: thesis: F # x is convergent

now

let n, m be Element of 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 C5, A3;
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;

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