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 E -measurable ) holds
(F || E) . n is E -measurable
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 E -measurable ) holds
(F || E) . n is E -measurable
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 E -measurable ) holds
(F || E) . n is E -measurable
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 E -measurable ) holds
(F || E) . n is E -measurable
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 E -measurable ) implies (F || E) . n is E -measurable )
set G = F || E;
A1: Re (F || E) = (Re F) || E by Th21;
A2: Im (F || E) = (Im F) || E by Th22;
assume F is with_the_same_dom ; :: thesis: ( not E c= dom (F . 0) or ex m being Nat st not F . m is E -measurable or (F || E) . n is E -measurable )
then A3: Re F is with_the_same_dom ;
then A4: Im F is with_the_same_dom by Th25;
assume A5: E c= dom (F . 0) ; :: thesis: ( ex m being Nat st not F . m is E -measurable or (F || E) . n is E -measurable )
assume A6: for m being Nat holds F . m is E -measurable ; :: thesis: (F || E) . n is E -measurable
A7: for m being Nat holds
( (Re F) . m is E -measurable & (Im F) . m is E -measurable )

proof

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

end;

E c= dom ((Im F) . 0) by A5, MESFUN7C:def 12;
then (Im (F || E)) . n is E -measurable by A4, A2, A7, Th4;
then A8: Im ((F || E) . n) is E -measurable by MESFUN7C:24;
E c= dom ((Re F) . 0) by A5, MESFUN7C:def 11;
then (Re (F || E)) . n is E -measurable by A3, A1, A7, Th4;
then Re ((F || E) . n) is E -measurable by MESFUN7C:24;
hence (F || E) . n is E -measurable by A8, MESFUN6C:def 1; :: thesis: verum