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

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

A3:
for n being Nat holds (Re F) . n is_integrable_on M
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;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

proof

thus
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
:: thesis: verum
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;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

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