let X be non empty set ; :: thesis: for S being SigmaField of X
for n being Nat
for F being Functional_Sequence of X,COMPLEX 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 n being Nat
for F being Functional_Sequence of X,COMPLEX 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 F being Functional_Sequence of X,COMPLEX 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,COMPLEX; :: 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 (Im F) . m is_simple_func_in S

proof

let m be Nat; :: thesis: (Im F) . m is_simple_func_in S
F . m is_simple_func_in S by A1;
then Im (F . m) is_simple_func_in S by MESFUN7C:43;
hence (Im F) . m is_simple_func_in S by MESFUN7C:24; :: thesis: verum

end;

then (Partial_Sums (Im F)) . n is_simple_func_in S by Th15;
then (Im (Partial_Sums F)) . n is_simple_func_in S by Th29;
then A2: Im ((Partial_Sums F) . n) is_simple_func_in S by MESFUN7C:24;
for m being Nat holds (Re F) . m is_simple_func_in S

proof

let m be Nat; :: thesis: (Re F) . m is_simple_func_in S
F . m is_simple_func_in S by A1;
then Re (F . m) is_simple_func_in S by MESFUN7C:43;
hence (Re F) . m is_simple_func_in S by MESFUN7C:24; :: thesis: verum

end;

then (Partial_Sums (Re F)) . n is_simple_func_in S by Th15;
then (Re (Partial_Sums F)) . n is_simple_func_in S by Th29;
then Re ((Partial_Sums F) . n) is_simple_func_in S by MESFUN7C:24;
hence (Partial_Sums F) . n is_simple_func_in S by A2, MESFUN7C:43; :: thesis: verum