let X be non empty set ; :: thesis: for S being SigmaField of X
for F being Functional_Sequence of X,REAL
for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let S be SigmaField of X; :: thesis: for F being Functional_Sequence of X,REAL
for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let F be Functional_Sequence of X,REAL; :: thesis: for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let n be Nat; :: thesis: ( ( for m being Nat holds F . m is_simple_func_in S ) implies (Partial_Sums F) . n is_simple_func_in S )
assume A1: for m being Nat holds F . m is_simple_func_in S ; :: thesis: (Partial_Sums F) . n is_simple_func_in S
for m being Nat holds (R_EAL F) . m is_simple_func_in S

proof

let m be Nat; :: thesis: (R_EAL F) . m is_simple_func_in S
F . m is_simple_func_in S by A1;
then R_EAL (F . m) is_simple_func_in S by MESFUNC6:49;
hence (R_EAL F) . m is_simple_func_in S ; :: thesis: verum

end;

then (Partial_Sums (R_EAL F)) . n is_simple_func_in S by MESFUNC9:35;
then (R_EAL (Partial_Sums F)) . n is_simple_func_in S by Th7;
then R_EAL ((Partial_Sums F) . n) is_simple_func_in S ;
hence (Partial_Sums F) . n is_simple_func_in S by MESFUNC6:49; :: thesis: verum