let X be non empty set ; :: thesis: for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,REAL

for n being Nat 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 F being Functional_Sequence of X,REAL

for n being Nat 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 F being Functional_Sequence of X,REAL

for n being Nat 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,REAL; :: thesis: for n being Nat 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: ( 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;

assume A1: ( F is with_the_same_dom & 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 A2: for m being Nat holds F . m is E -measurable ; :: thesis: (F || E) . n is E -measurable

for m being Nat holds

( (R_EAL F) . m is E -measurable & (R_EAL (F || E)) . m = ((R_EAL F) . m) | E )

hence (F || E) . n is E -measurable ; :: thesis: verum

for E being Element of S

for F being Functional_Sequence of X,REAL

for n being Nat 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 F being Functional_Sequence of X,REAL

for n being Nat 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 F being Functional_Sequence of X,REAL

for n being Nat 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,REAL; :: thesis: for n being Nat 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: ( 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;

assume A1: ( F is with_the_same_dom & 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 A2: for m being Nat holds F . m is E -measurable ; :: thesis: (F || E) . n is E -measurable

for m being Nat holds

( (R_EAL F) . m is E -measurable & (R_EAL (F || E)) . m = ((R_EAL F) . m) | E )

proof

then
R_EAL ((F || E) . n) is E -measurable
by A1, MESFUNC9:20;
let m be Nat; :: thesis: ( (R_EAL F) . m is E -measurable & (R_EAL (F || E)) . m = ((R_EAL F) . m) | E )

F . m is E -measurable by A2;

then R_EAL (F . m) is E -measurable ;

hence (R_EAL F) . m is E -measurable ; :: thesis: (R_EAL (F || E)) . m = ((R_EAL F) . m) | E

thus (R_EAL (F || E)) . m = ((R_EAL F) . m) | E by Def1; :: thesis: verum

end;F . m is E -measurable by A2;

then R_EAL (F . m) is E -measurable ;

hence (R_EAL F) . m is E -measurable ; :: thesis: (R_EAL (F || E)) . m = ((R_EAL F) . m) | E

thus (R_EAL (F || E)) . m = ((R_EAL F) . m) | E by Def1; :: thesis: verum

hence (F || E) . n is E -measurable ; :: thesis: verum