let X be non empty set ; :: thesis: for S being SigmaField of X

for E being Element of S

for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let E be Element of S; :: thesis: for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let m be Nat; :: thesis: for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( ( for n being Nat holds F . n is E -measurable ) implies (Partial_Sums F) . m is E -measurable )

assume A1: for n being Nat holds F . n is E -measurable ; :: thesis: (Partial_Sums F) . m is E -measurable

then for n being Nat holds (Im F) . n is E -measurable by Lm2;

then (Partial_Sums (Im F)) . m is E -measurable by Th16;

then (Im (Partial_Sums F)) . m is E -measurable by Th29;

then A2: Im ((Partial_Sums F) . m) is E -measurable by MESFUN7C:24;

for n being Nat holds (Re F) . n is E -measurable by A1, Lm2;

then (Partial_Sums (Re F)) . m is E -measurable by Th16;

then (Re (Partial_Sums F)) . m is E -measurable by Th29;

then Re ((Partial_Sums F) . m) is E -measurable by MESFUN7C:24;

hence (Partial_Sums F) . m is E -measurable by A2, MESFUN6C:def 1; :: thesis: verum

for E being Element of S

for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let E be Element of S; :: thesis: for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let m be Nat; :: thesis: for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( ( for n being Nat holds F . n is E -measurable ) implies (Partial_Sums F) . m is E -measurable )

assume A1: for n being Nat holds F . n is E -measurable ; :: thesis: (Partial_Sums F) . m is E -measurable

then for n being Nat holds (Im F) . n is E -measurable by Lm2;

then (Partial_Sums (Im F)) . m is E -measurable by Th16;

then (Im (Partial_Sums F)) . m is E -measurable by Th29;

then A2: Im ((Partial_Sums F) . m) is E -measurable by MESFUN7C:24;

for n being Nat holds (Re F) . n is E -measurable by A1, Lm2;

then (Partial_Sums (Re F)) . m is E -measurable by Th16;

then (Re (Partial_Sums F)) . m is E -measurable by Th29;

then Re ((Partial_Sums F) . m) is E -measurable by MESFUN7C:24;

hence (Partial_Sums F) . m is E -measurable by A2, MESFUN6C:def 1; :: thesis: verum