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 )

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

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

E c= dom ((Im F) . 0)
by A5, MESFUN7C:def 12;
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;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

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