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

( (Re F) . m is E -measurable & (Im 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

( (Re F) . m is E -measurable & (Im 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

( (Re F) . m is E -measurable & (Im 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

( (Re F) . m is E -measurable & (Im 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 ( (Re F) . m is E -measurable & (Im F) . m is E -measurable ) )

assume for n being Nat holds F . n is E -measurable ; :: thesis: ( (Re F) . m is E -measurable & (Im F) . m is E -measurable )

then F . m is E -measurable ;

then ( Re (F . m) is E -measurable & Im (F . m) is E -measurable ) by MESFUN6C:def 1;

hence ( (Re F) . m is E -measurable & (Im F) . m is E -measurable ) by MESFUN7C:24; :: 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

( (Re F) . m is E -measurable & (Im 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

( (Re F) . m is E -measurable & (Im 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

( (Re F) . m is E -measurable & (Im 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

( (Re F) . m is E -measurable & (Im 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 ( (Re F) . m is E -measurable & (Im F) . m is E -measurable ) )

assume for n being Nat holds F . n is E -measurable ; :: thesis: ( (Re F) . m is E -measurable & (Im F) . m is E -measurable )

then F . m is E -measurable ;

then ( Re (F . m) is E -measurable & Im (F . m) is E -measurable ) by MESFUN6C:def 1;

hence ( (Re F) . m is E -measurable & (Im F) . m is E -measurable ) by MESFUN7C:24; :: thesis: verum