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 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:70;
then A8: |.((F . 0 ) . x).| = (F . 0 ) . x by EXTREAL1:def 3;
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_measurable_on E by A2;
then Integral M,(F . 0 ) = integral+ M,(F . 0 ) by A1, A5, MESFUNC5:94;
then integral+ M,(F . 0 ) < +infty by A1, A4, RELAT_1:97;
then A10: integral+ M,|.(F . 0 ).| < +infty by A6, A7, PARTFUN1:34;
A11: max+ (F . 0 ) is_measurable_on E by A2, MESFUNC2:27;
for x being set st x in dom (max- (F . 0 )) holds
0. <= (max- (F . 0 )) . x by MESFUNC2:15;
then A12: max- (F . 0 ) is nonnegative by SUPINF_2:71;
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:70;
then |.((F . n) . x).| = (F . n) . x by EXTREAL1:def 3;
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

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 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:97;
for x being set st x in dom (max+ (F . 0 )) holds
0. <= (max+ (F . 0 )) . x by MESFUNC2:14;
then A20: max+ (F . 0 ) is nonnegative by SUPINF_2:71;
then A21: dom ((max+ (F . 0 )) + (max- (F . 0 ))) = (dom (max+ (F . 0 ))) /\ (dom (max- (F . 0 ))) by A12, MESFUNC5:28;
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:97;
max- (F . 0 ) is_measurable_on E by A1, A2, MESFUNC2:28;
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:84;
then A24: (integral+ M,(max+ (F . 0 ))) + (integral+ M,(max- (F . 0 ))) < +infty by A1, A18, A22, A21, A19, A23, A10, MESFUNC2:26;
0 <= integral+ M,(max- (F . 0 )) by A1, A9, A22, A12, MESFUNC2:28, MESFUNC5:85;
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:27, MESFUNC5:85;
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, MESFUNC5:def 17;
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, A5, A13, Th18;
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