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

for E being Element of S

for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let E be Element of S; :: thesis: for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) implies lim (Partial_Sums F) is E -measurable )

assume that

A1: dom (F . 0) = E and

A2: F is with_the_same_dom and

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

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

F # x is summable ; :: thesis: lim (Partial_Sums F) is E -measurable

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

A6: for x being Element of X st x in dom ((Partial_Sums F) . 0) holds

(Partial_Sums F) # x is convergent

(Im F) # x is summable

then Im F is with_the_same_dom by Th25;

then lim (Partial_Sums (Im F)) is E -measurable by A5, A9, A10, Th18;

then A13: lim (Im (Partial_Sums F)) is E -measurable by Th29;

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

(Re F) # x is summable

then lim (Im (Partial_Sums F)) = R_EAL (Im (lim (Partial_Sums F))) by A6, MESFUN7C:25;

then A18: Im (lim (Partial_Sums F)) is E -measurable by A13;

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

then lim (Partial_Sums (Re F)) is E -measurable by A12, A16, A14, Th18;

then A19: lim (Re (Partial_Sums F)) is E -measurable by Th29;

lim (Re (Partial_Sums F)) = R_EAL (Re (lim (Partial_Sums F))) by A6, A17, MESFUN7C:25;

then Re (lim (Partial_Sums F)) is E -measurable by A19;

hence lim (Partial_Sums F) is E -measurable by A18, MESFUN6C:def 1; :: thesis: verum

for E being Element of S

for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let E be Element of S; :: thesis: for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) implies lim (Partial_Sums F) is E -measurable )

assume that

A1: dom (F . 0) = E and

A2: F is with_the_same_dom and

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

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

F # x is summable ; :: thesis: lim (Partial_Sums F) is E -measurable

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

A6: for x being Element of X st x in dom ((Partial_Sums F) . 0) holds

(Partial_Sums F) # x is convergent

proof

A9:
for n being Nat holds (Partial_Sums (Im F)) . n is E -measurable
let x be Element of X; :: thesis: ( x in dom ((Partial_Sums F) . 0) implies (Partial_Sums F) # x is convergent )

assume A7: x in dom ((Partial_Sums F) . 0) ; :: thesis: (Partial_Sums F) # x is convergent

A8: dom ((Partial_Sums F) . 0) = dom (F . 0) by A2, Th32;

then F # x is summable by A1, A4, A7;

then Partial_Sums (F # x) is convergent ;

hence (Partial_Sums F) # x is convergent by A2, A7, A8, Th35; :: thesis: verum

end;assume A7: x in dom ((Partial_Sums F) . 0) ; :: thesis: (Partial_Sums F) # x is convergent

A8: dom ((Partial_Sums F) . 0) = dom (F . 0) by A2, Th32;

then F # x is summable by A1, A4, A7;

then Partial_Sums (F # x) is convergent ;

hence (Partial_Sums F) # x is convergent by A2, A7, A8, Th35; :: thesis: verum

proof

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

(Partial_Sums F) . n is E -measurable by A3;

then Im ((Partial_Sums F) . n) is E -measurable by MESFUN6C:def 1;

then (Im (Partial_Sums F)) . n is E -measurable by MESFUN7C:24;

hence (Partial_Sums (Im F)) . n is E -measurable by Th29; :: thesis: verum

end;(Partial_Sums F) . n is E -measurable by A3;

then Im ((Partial_Sums F) . n) is E -measurable by MESFUN6C:def 1;

then (Im (Partial_Sums F)) . n is E -measurable by MESFUN7C:24;

hence (Partial_Sums (Im F)) . n is E -measurable by Th29; :: thesis: verum

(Im F) # x is summable

proof

A12:
Re F is with_the_same_dom
by A2;
let x be Element of X; :: thesis: ( x in E implies (Im F) # x is summable )

assume A11: x in E ; :: thesis: (Im F) # x is summable

then F # x is summable by A4;

then Im (F # x) is summable ;

hence (Im F) # x is summable by A1, A2, A11, MESFUN7C:23; :: thesis: verum

end;assume A11: x in E ; :: thesis: (Im F) # x is summable

then F # x is summable by A4;

then Im (F # x) is summable ;

hence (Im F) # x is summable by A1, A2, A11, MESFUN7C:23; :: thesis: verum

then Im F is with_the_same_dom by Th25;

then lim (Partial_Sums (Im F)) is E -measurable by A5, A9, A10, Th18;

then A13: lim (Im (Partial_Sums F)) is E -measurable by Th29;

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

(Re F) # x is summable

proof

A16:
for n being Nat holds (Partial_Sums (Re F)) . n is E -measurable
let x be Element of X; :: thesis: ( x in E implies (Re F) # x is summable )

assume A15: x in E ; :: thesis: (Re F) # x is summable

then F # x is summable by A4;

then Re (F # x) is summable ;

hence (Re F) # x is summable by A1, A2, A15, MESFUN7C:23; :: thesis: verum

end;assume A15: x in E ; :: thesis: (Re F) # x is summable

then F # x is summable by A4;

then Re (F # x) is summable ;

hence (Re F) # x is summable by A1, A2, A15, MESFUN7C:23; :: thesis: verum

proof

A17:
Partial_Sums F is with_the_same_dom
by A2, Th34;
let n be Nat; :: thesis: (Partial_Sums (Re F)) . n is E -measurable

(Partial_Sums F) . n is E -measurable by A3;

then Re ((Partial_Sums F) . n) is E -measurable by MESFUN6C:def 1;

then (Re (Partial_Sums F)) . n is E -measurable by MESFUN7C:24;

hence (Partial_Sums (Re F)) . n is E -measurable by Th29; :: thesis: verum

end;(Partial_Sums F) . n is E -measurable by A3;

then Re ((Partial_Sums F) . n) is E -measurable by MESFUN6C:def 1;

then (Re (Partial_Sums F)) . n is E -measurable by MESFUN7C:24;

hence (Partial_Sums (Re F)) . n is E -measurable by Th29; :: thesis: verum

then lim (Im (Partial_Sums F)) = R_EAL (Im (lim (Partial_Sums F))) by A6, MESFUN7C:25;

then A18: Im (lim (Partial_Sums F)) is E -measurable by A13;

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

then lim (Partial_Sums (Re F)) is E -measurable by A12, A16, A14, Th18;

then A19: lim (Re (Partial_Sums F)) is E -measurable by Th29;

lim (Re (Partial_Sums F)) = R_EAL (Re (lim (Partial_Sums F))) by A6, A17, MESFUN7C:25;

then Re (lim (Partial_Sums F)) is E -measurable by A19;

hence lim (Partial_Sums F) is E -measurable by A18, MESFUN6C:def 1; :: thesis: verum