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

proof

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;

A9: for n being Nat holds (Partial_Sums (Im F)) . n is E -measurable

proof

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;

A10: for x being Element of X st x in E holds
(Im F) # x is summable

proof

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;

A12: Re F is with_the_same_dom by A2;
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

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;

A16: for n being Nat holds (Partial_Sums (Re F)) . n is E -measurable

proof

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;

A17: Partial_Sums F is with_the_same_dom by A2, Th34;
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