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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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: for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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,COMPLEX; :: 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) 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 and

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

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

A7: for n being Nat holds

( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) by A3, Lm2;

for x being Element of X

for n being Nat st x in E holds

( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

for n being Nat holds

( ( x in E implies |.((Re F) . n).| . x <= P . x ) & ( x in E implies |.((Im F) . n).| . x <= P . x ) ) ;

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

( (Re F) # x is convergent & (Im F) # x is convergent )

(Im F) # x is convergent ;

E = dom ((Im F) . 0) by A1, MESFUN7C:def 12;

then lim (Im F) is_integrable_on M by A2, A4, A7, A13, A16, Th47;

then R_EAL (Im (lim F)) is_integrable_on M by A1, A6, MESFUN7C:25;

then A17: Im (lim F) is_integrable_on M ;

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

(Re F) # x is convergent by A14;

E = dom ((Re F) . 0) by A1, MESFUN7C:def 11;

then lim (Re F) is_integrable_on M by A2, A4, A7, A13, A18, Th47;

then R_EAL (Re (lim F)) is_integrable_on M by A1, A6, MESFUN7C:25;

then Re (lim F) is_integrable_on M ;

hence lim F is_integrable_on M by A17, MESFUN6C:def 2; :: thesis: verum

for M being sigma_Measure of S

for E being Element of S

for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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: for F being with_the_same_dom Functional_Sequence of X,COMPLEX 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,COMPLEX; :: 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) 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 and

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

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

A7: for n being Nat holds

( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) by A3, Lm2;

for x being Element of X

for n being Nat st x in E holds

( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

proof

then A13:
for x being Element of X
let x be Element of X; :: thesis: for n being Nat st x in E holds

( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

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

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

Re ((F # x) . n1) = (Re (F # x)) . n1 by COMSEQ_3:def 5;

then A8: |.((Re (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

Im ((F # x) . n1) = (Im (F # x)) . n1 by COMSEQ_3:def 6;

then A9: |.((Im (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

assume A10: x in E ; :: thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

then |.(F . n).| . x <= P . x by A5;

then |.((F . n) . x).| <= P . x by VALUED_1:18;

then A11: |.((F # x) . n).| <= P . x by MESFUN7C:def 9;

(Im F) # x = Im (F # x) by A1, A10, MESFUN7C:23;

then |.(((Im F) # x) . n1).| <= P . x by A11, A9, XXREAL_0:2;

then A12: |.(((Im F) . n1) . x).| <= P . x by SEQFUNC:def 10;

(Re F) # x = Re (F # x) by A1, A10, MESFUN7C:23;

then |.(((Re F) # x) . n1).| <= P . x by A11, A8, XXREAL_0:2;

then |.(((Re F) . n1) . x).| <= P . x by SEQFUNC:def 10;

hence ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by A12, VALUED_1:18; :: thesis: verum

end;( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

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

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

Re ((F # x) . n1) = (Re (F # x)) . n1 by COMSEQ_3:def 5;

then A8: |.((Re (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

Im ((F # x) . n1) = (Im (F # x)) . n1 by COMSEQ_3:def 6;

then A9: |.((Im (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

assume A10: x in E ; :: thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

then |.(F . n).| . x <= P . x by A5;

then |.((F . n) . x).| <= P . x by VALUED_1:18;

then A11: |.((F # x) . n).| <= P . x by MESFUN7C:def 9;

(Im F) # x = Im (F # x) by A1, A10, MESFUN7C:23;

then |.(((Im F) # x) . n1).| <= P . x by A11, A9, XXREAL_0:2;

then A12: |.(((Im F) . n1) . x).| <= P . x by SEQFUNC:def 10;

(Re F) # x = Re (F # x) by A1, A10, MESFUN7C:23;

then |.(((Re F) # x) . n1).| <= P . x by A11, A8, XXREAL_0:2;

then |.(((Re F) . n1) . x).| <= P . x by SEQFUNC:def 10;

hence ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by A12, VALUED_1:18; :: thesis: verum

for n being Nat holds

( ( x in E implies |.((Re F) . n).| . x <= P . x ) & ( x in E implies |.((Im F) . n).| . x <= P . x ) ) ;

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

( (Re F) # x is convergent & (Im F) # x is convergent )

proof

then A16:
for x being Element of X st x in E holds
let x be Element of X; :: thesis: ( x in E implies ( (Re F) # x is convergent & (Im F) # x is convergent ) )

assume A15: x in E ; :: thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )

then F # x is convergent Complex_Sequence by A6;

then ( Re (F # x) is convergent & Im (F # x) is convergent ) ;

hence ( (Re F) # x is convergent & (Im F) # x is convergent ) by A1, A15, MESFUN7C:23; :: thesis: verum

end;assume A15: x in E ; :: thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )

then F # x is convergent Complex_Sequence by A6;

then ( Re (F # x) is convergent & Im (F # x) is convergent ) ;

hence ( (Re F) # x is convergent & (Im F) # x is convergent ) by A1, A15, MESFUN7C:23; :: thesis: verum

(Im F) # x is convergent ;

E = dom ((Im F) . 0) by A1, MESFUN7C:def 12;

then lim (Im F) is_integrable_on M by A2, A4, A7, A13, A16, Th47;

then R_EAL (Im (lim F)) is_integrable_on M by A1, A6, MESFUN7C:25;

then A17: Im (lim F) is_integrable_on M ;

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

(Re F) # x is convergent by A14;

E = dom ((Re F) . 0) by A1, MESFUN7C:def 11;

then lim (Re F) is_integrable_on M by A2, A4, A7, A13, A18, Th47;

then R_EAL (Re (lim F)) is_integrable_on M by A1, A6, MESFUN7C:25;

then Re (lim F) is_integrable_on M ;

hence lim F is_integrable_on M by A17, MESFUN6C:def 2; :: thesis: verum