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,REAL 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,REAL 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,REAL 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,REAL; :: 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

let m be Nat; :: thesis: (Partial_Sums F) . m is_integrable_on M

for n being Nat holds (R_EAL F) . n is_integrable_on M

then (R_EAL (Partial_Sums F)) . m is_integrable_on M by Th7;

then R_EAL ((Partial_Sums F) . m) is_integrable_on M ;

hence (Partial_Sums F) . m is_integrable_on M ; :: thesis: verum

for M being sigma_Measure of S

for F being Functional_Sequence of X,REAL 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,REAL 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,REAL 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,REAL; :: 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

let m be Nat; :: thesis: (Partial_Sums F) . m is_integrable_on M

for n being Nat holds (R_EAL F) . n is_integrable_on M

proof

then
(Partial_Sums (R_EAL F)) . m is_integrable_on M
by MESFUNC9:45;
let n be Nat; :: thesis: (R_EAL F) . n is_integrable_on M

F . n is_integrable_on M by A1;

then R_EAL (F . n) is_integrable_on M ;

hence (R_EAL F) . n is_integrable_on M ; :: thesis: verum

end;F . n is_integrable_on M by A1;

then R_EAL (F . n) is_integrable_on M ;

hence (R_EAL F) . n is_integrable_on M ; :: thesis: verum

then (R_EAL (Partial_Sums F)) . m is_integrable_on M by Th7;

then R_EAL ((Partial_Sums F) . m) is_integrable_on M ;

hence (Partial_Sums F) . m is_integrable_on M ; :: thesis: verum