let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let M be sigma_Measure of S; :: thesis: for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let F be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let P be PartFunc of X,REAL; :: thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) implies ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) ) )

assume that

A1: E = dom (F . 0) and

A2: E = dom P and

A3: for n being Nat holds F . n is E -measurable and

A4: P is_integrable_on M and

A5: for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ; :: thesis: ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

A6: R_EAL P is_integrable_on M by A4;

A7: for x being Element of X

for n being Nat st x in E holds

|.((R_EAL F) . n).| . x <= (R_EAL P) . x

then consider J being ExtREAL_sequence such that

A11: for n being Nat holds J . n = Integral (M,((R_EAL F) . n)) and

lim_inf J >= Integral (M,(lim_inf (R_EAL F))) and

lim_sup J <= Integral (M,(lim_sup (R_EAL F))) and

A12: ( ( for x being Element of X st x in E holds

(R_EAL F) # x is convergent ) implies ( J is convergent & lim J = Integral (M,(lim (R_EAL F))) ) ) by A1, A2, A9, A6, A7, MESFUN10:17;

A13: Integral (M,(R_EAL P)) < +infty by A6, MESFUNC5:96;

for n being Nat holds |.(J . n).| < +infty

|.(J . n).| < +infty ;

then J is V61() by MESFUNC2:def 1;

then reconsider I = J as Real_Sequence by RINFSUP2:6;

( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) ) )

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) by RINFSUP2:15;

for n being Nat holds I . n = Integral (M,(F . n)) by A11;

hence ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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 A22; :: thesis: verum

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let M be sigma_Measure of S; :: thesis: for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let F be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

let P be PartFunc of X,REAL; :: thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) implies ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) ) )

assume that

A1: E = dom (F . 0) and

A2: E = dom P and

A3: for n being Nat holds F . n is E -measurable and

A4: P is_integrable_on M and

A5: for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ; :: thesis: ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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)) ) ) )

A6: R_EAL P is_integrable_on M by A4;

A7: for x being Element of X

for n being Nat st x in E holds

|.((R_EAL F) . n).| . x <= (R_EAL P) . x

proof

A9:
for n being Nat holds (R_EAL F) . n is E -measurable
let x be Element of X; :: thesis: for n being Nat st x in E holds

|.((R_EAL F) . n).| . x <= (R_EAL P) . x

let n be Nat; :: thesis: ( x in E implies |.((R_EAL F) . n).| . x <= (R_EAL P) . x )

A8: R_EAL |.(F . n).| = |.(R_EAL (F . n)).| by MESFUNC6:1;

assume x in E ; :: thesis: |.((R_EAL F) . n).| . x <= (R_EAL P) . x

hence |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A5, A8; :: thesis: verum

end;|.((R_EAL F) . n).| . x <= (R_EAL P) . x

let n be Nat; :: thesis: ( x in E implies |.((R_EAL F) . n).| . x <= (R_EAL P) . x )

A8: R_EAL |.(F . n).| = |.(R_EAL (F . n)).| by MESFUNC6:1;

assume x in E ; :: thesis: |.((R_EAL F) . n).| . x <= (R_EAL P) . x

hence |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A5, A8; :: thesis: verum

proof

let n be Nat; :: thesis: (R_EAL F) . n is E -measurable

F . n is E -measurable by A3;

then R_EAL (F . n) is E -measurable ;

hence (R_EAL F) . n is E -measurable ; :: thesis: verum

end;F . n is E -measurable by A3;

then R_EAL (F . n) is E -measurable ;

hence (R_EAL F) . n is E -measurable ; :: thesis: verum

now :: thesis: for x being object st x in dom P holds

0 <= P . x

then
P is nonnegative
by MESFUNC6:52;0 <= P . x

let x be object ; :: thesis: ( x in dom P implies 0 <= P . x )

assume A10: x in dom P ; :: thesis: 0 <= P . x

then x in dom |.(F . 0).| by A1, A2, VALUED_1:def 11;

then |.(F . 0).| . x = |.((F . 0) . x).| by VALUED_1:def 11;

then |.((F . 0) . x).| <= P . x by A2, A5, A10;

hence 0 <= P . x by COMPLEX1:46; :: thesis: verum

end;assume A10: x in dom P ; :: thesis: 0 <= P . x

then x in dom |.(F . 0).| by A1, A2, VALUED_1:def 11;

then |.(F . 0).| . x = |.((F . 0) . x).| by VALUED_1:def 11;

then |.((F . 0) . x).| <= P . x by A2, A5, A10;

hence 0 <= P . x by COMPLEX1:46; :: thesis: verum

then consider J being ExtREAL_sequence such that

A11: for n being Nat holds J . n = Integral (M,((R_EAL F) . n)) and

lim_inf J >= Integral (M,(lim_inf (R_EAL F))) and

lim_sup J <= Integral (M,(lim_sup (R_EAL F))) and

A12: ( ( for x being Element of X st x in E holds

(R_EAL F) # x is convergent ) implies ( J is convergent & lim J = Integral (M,(lim (R_EAL F))) ) ) by A1, A2, A9, A6, A7, MESFUN10:17;

A13: Integral (M,(R_EAL P)) < +infty by A6, MESFUNC5:96;

for n being Nat holds |.(J . n).| < +infty

proof

then
for n being Element of NAT st n in dom J holds
let n be Nat; :: thesis: |.(J . n).| < +infty

A14: ( E = dom ((R_EAL F) . n) & (R_EAL F) . n is E -measurable ) by A1, A9, MESFUNC8:def 2;

|.((R_EAL F) . n).| is_integrable_on M by A1, A2, A9, A6, A7, MESFUN10:16;

then (R_EAL F) . n is_integrable_on M by A14, MESFUNC5:100;

then A15: |.(Integral (M,((R_EAL F) . n))).| <= Integral (M,|.((R_EAL F) . n).|) by MESFUNC5:101;

for x being Element of X st x in dom ((R_EAL F) . n) holds

|.(((R_EAL F) . n) . x).| <= (R_EAL P) . x

then |.(Integral (M,((R_EAL F) . n))).| <= Integral (M,(R_EAL P)) by A15, XXREAL_0:2;

then |.(Integral (M,((R_EAL F) . n))).| < +infty by A13, XXREAL_0:2;

hence |.(J . n).| < +infty by A11; :: thesis: verum

end;A14: ( E = dom ((R_EAL F) . n) & (R_EAL F) . n is E -measurable ) by A1, A9, MESFUNC8:def 2;

|.((R_EAL F) . n).| is_integrable_on M by A1, A2, A9, A6, A7, MESFUN10:16;

then (R_EAL F) . n is_integrable_on M by A14, MESFUNC5:100;

then A15: |.(Integral (M,((R_EAL F) . n))).| <= Integral (M,|.((R_EAL F) . n).|) by MESFUNC5:101;

for x being Element of X st x in dom ((R_EAL F) . n) holds

|.(((R_EAL F) . n) . x).| <= (R_EAL P) . x

proof

then
Integral (M,|.((R_EAL F) . n).|) <= Integral (M,(R_EAL P))
by A2, A6, A14, MESFUNC5:102;
let x be Element of X; :: thesis: ( x in dom ((R_EAL F) . n) implies |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x )

assume A16: x in dom ((R_EAL F) . n) ; :: thesis: |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x

then x in E by A1, MESFUNC8:def 2;

then A17: |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A7;

x in dom |.((R_EAL F) . n).| by A16, MESFUNC1:def 10;

hence |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x by A17, MESFUNC1:def 10; :: thesis: verum

end;assume A16: x in dom ((R_EAL F) . n) ; :: thesis: |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x

then x in E by A1, MESFUNC8:def 2;

then A17: |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A7;

x in dom |.((R_EAL F) . n).| by A16, MESFUNC1:def 10;

hence |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x by A17, MESFUNC1:def 10; :: thesis: verum

then |.(Integral (M,((R_EAL F) . n))).| <= Integral (M,(R_EAL P)) by A15, XXREAL_0:2;

then |.(Integral (M,((R_EAL F) . n))).| < +infty by A13, XXREAL_0:2;

hence |.(J . n).| < +infty by A11; :: thesis: verum

|.(J . n).| < +infty ;

then J is V61() by MESFUNC2:def 1;

then reconsider I = J as Real_Sequence by RINFSUP2:6;

( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) ) )

proof

then A22:
( ( for x being Element of X st x in E holds
assume A18:
for x being Element of X st x in E holds

F # x is convergent ; :: thesis: ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) )

then A21: ( -infty < Integral (M,(lim F)) & Integral (M,(lim F)) < +infty ) by MESFUNC5:96;

( J is convergent implies J is convergent_to_finite_number ) by A12, A19, A21, MESFUNC5:def 12;

hence ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) ) by A12, A19; :: thesis: verum

end;F # x is convergent ; :: thesis: ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) )

A19: now :: thesis: for x being Element of X st x in E holds

(R_EAL F) # x is convergent

lim F is_integrable_on M
by A1, A2, A3, A4, A5, A18, Th47;(R_EAL F) # x is convergent

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

assume x in E ; :: thesis: (R_EAL F) # x is convergent

then A20: F # x is convergent by A18;

F # x = (R_EAL F) # x by MESFUN7C:1;

hence (R_EAL F) # x is convergent by A20, RINFSUP2:14; :: thesis: verum

end;assume x in E ; :: thesis: (R_EAL F) # x is convergent

then A20: F # x is convergent by A18;

F # x = (R_EAL F) # x by MESFUN7C:1;

hence (R_EAL F) # x is convergent by A20, RINFSUP2:14; :: thesis: verum

then A21: ( -infty < Integral (M,(lim F)) & Integral (M,(lim F)) < +infty ) by MESFUNC5:96;

( J is convergent implies J is convergent_to_finite_number ) by A12, A19, A21, MESFUNC5:def 12;

hence ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) ) by A12, A19; :: thesis: verum

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) by RINFSUP2:15;

for n being Nat holds I . n = Integral (M,(F . n)) by A11;

hence ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( 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 A22; :: thesis: verum