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_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
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_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
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_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let m be Nat; :: thesis: for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let F be Functional_Sequence of X,COMPLEX; :: thesis: ( ( for n being Nat holds F . n is_measurable_on E ) implies (Partial_Sums F) . m is_measurable_on E )
assume A1: for n being Nat holds F . n is_measurable_on E ; :: thesis: (Partial_Sums F) . m is_measurable_on E
then for n being Nat holds (Im F) . n is_measurable_on E by Lm2;
then (Partial_Sums (Im F)) . m is_measurable_on E by Th16;
then (Im (Partial_Sums F)) . m is_measurable_on E by Th29;
then A2: Im ((Partial_Sums F) . m) is_measurable_on E by MESFUN7C:24;
for n being Nat holds (Re F) . n is_measurable_on E by A1, Lm2;
then (Partial_Sums (Re F)) . m is_measurable_on E by Th16;
then (Re (Partial_Sums F)) . m is_measurable_on E by Th29;
then Re ((Partial_Sums F) . m) is_measurable_on E by MESFUN7C:24;
hence (Partial_Sums F) . m is_measurable_on E by A2, MESFUN6C:def 1; :: thesis: verum