let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0 ) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let S be SigmaField of X; :: thesis: for E being Element of S
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0 ) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let E be Element of S; :: thesis: for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0 ) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let n be Nat; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0 ) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let F be Functional_Sequence of X,COMPLEX ; :: thesis: ( F is with_the_same_dom & E c= dom (F . 0 ) & ( for m being Nat holds F . m is_measurable_on E ) implies (F || E) . n is_measurable_on E )
set G = F || E;
assume F is with_the_same_dom ; :: thesis: ( not E c= dom (F . 0 ) or ex m being Nat st not F . m is_measurable_on E or (F || E) . n is_measurable_on E )
then B0: Re F is with_the_same_dom by Lm33a;
then B3: Im F is with_the_same_dom by Lm33b;
assume E c= dom (F . 0 ) ; :: thesis: ( ex m being Nat st not F . m is_measurable_on E or (F || E) . n is_measurable_on E )
then B1: ( E c= dom ((Re F) . 0 ) & E c= dom ((Im F) . 0 ) ) by MESFUN7C:def 11, MESFUN7C:def 12;
assume A2: for m being Nat holds F . m is_measurable_on E ; :: thesis: (F || E) . n is_measurable_on E
aa: ( Re (F || E) = (Re F) || E & Im (F || E) = (Im F) || E ) by Lm31, Lm32;
for m being Nat holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )

proof

let m be Nat; :: thesis: ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
F . m is_measurable_on E by A2;
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

end;

then ( (Re (F || E)) . n is_measurable_on E & (Im (F || E)) . n is_measurable_on E ) by aa, B0, B1, B3, Th9;
then ( Re ((F || E) . n) is_measurable_on E & Im ((F || E) . n) is_measurable_on E ) by MESFUN7C:24;
hence (F || E) . n is_measurable_on E by MESFUN6C:def 3; :: thesis: verum