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

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

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

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

then
(Partial_Sums (Im F)) . n is_simple_func_in S
by Th15;
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;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

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

then
(Partial_Sums (Re F)) . n is_simple_func_in S
by Th15;
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;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

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