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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) implies lim F is_integrable_on M )

assume that

A1: ( E = dom (F . 0) & E = dom P ) and

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

A3: P is_integrable_on M and

A4: for x being Element of X

for n being Nat st x in E holds

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

A5: for x being Element of X st x in E holds

F # x is convergent ; :: thesis: lim F is_integrable_on M

A6: for n being Nat holds (R_EAL F) . n is E -measurable

(R_EAL F) # x is convergent

for n being Nat st x in E holds

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

hence lim F is_integrable_on M by A1, A6, A9, A7, Th46; :: 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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

lim F is_integrable_on M

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 ) & ( for x being Element of X st x in E holds

F # x is convergent ) implies lim F is_integrable_on M )

assume that

A1: ( E = dom (F . 0) & E = dom P ) and

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

A3: P is_integrable_on M and

A4: for x being Element of X

for n being Nat st x in E holds

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

A5: for x being Element of X st x in E holds

F # x is convergent ; :: thesis: lim F is_integrable_on M

A6: for n being Nat holds (R_EAL F) . n is E -measurable

proof

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

F . n is E -measurable by A2;

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 A2;

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

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

(R_EAL F) # x is convergent

proof

A9:
for x being Element of X
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 A8: F # x is convergent by A5;

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

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

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

then A8: F # x is convergent by A5;

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

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

for n being Nat st x in E holds

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

proof

R_EAL P is_integrable_on M
by A3;
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 )

A10: 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 A4, A10; :: 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 )

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

hence lim F is_integrable_on M by A1, A6, A9, A7, Th46; :: thesis: verum