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
( (Re F) . m is_measurable_on E & (Im 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
( (Re F) . m is_measurable_on E & (Im 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
( (Re F) . m is_measurable_on E & (Im 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
( (Re F) . m is_measurable_on E & (Im 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 ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E ) )
assume for n being Nat holds F . n is_measurable_on E ; :: thesis: ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
then F . m is_measurable_on E ;
then ( Re (F . m) is_measurable_on E & Im (F . m) is_measurable_on E ) by MESFUN6C:def 3;
hence ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E ) by MESFUN7C:24; :: thesis: verum