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

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

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

then
(Partial_Sums (R_EAL F)) . n is_simple_func_in S
by MESFUNC9:35;
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;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

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