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

proof

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;

then (Partial_Sums (R_EAL F)) . m is_integrable_on M by MESFUNC9:45;
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