let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let F be Functional_Sequence of X,COMPLEX; :: thesis: ( ( for n being Nat holds F . n is_integrable_on M ) implies for m being Nat holds (Partial_Sums F) . m is_integrable_on M )
assume A1: for n being Nat holds F . n is_integrable_on M ; :: thesis: for m being Nat holds (Partial_Sums F) . m is_integrable_on M
A2: for n being Nat holds (Im F) . n is_integrable_on M

proof

let n be Nat; :: thesis: (Im F) . n is_integrable_on M
F . n is_integrable_on M by A1;
then Im (F . n) is_integrable_on M by MESFUN6C:def 2;
hence (Im F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum

end;

A3: for n being Nat holds (Re F) . n is_integrable_on M

proof

let n be Nat; :: thesis: (Re F) . n is_integrable_on M
F . n is_integrable_on M by A1;
then Re (F . n) is_integrable_on M by MESFUN6C:def 2;
hence (Re F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum

end;

thus for m being Nat holds (Partial_Sums F) . m is_integrable_on M :: thesis: verum

proof

let m be Nat; :: thesis: (Partial_Sums F) . m is_integrable_on M
(Partial_Sums (Im F)) . m is_integrable_on M by A2, Th19;
then (Im (Partial_Sums F)) . m is_integrable_on M by Th29;
then A4: Im ((Partial_Sums F) . m) is_integrable_on M by MESFUN7C:24;
(Partial_Sums (Re F)) . m is_integrable_on M by A3, Th19;
then (Re (Partial_Sums F)) . m is_integrable_on M by Th29;
then Re ((Partial_Sums F) . m) is_integrable_on M by MESFUN7C:24;
hence (Partial_Sums F) . m is_integrable_on M by A4, MESFUN6C:def 2; :: thesis: verum

end;