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 )

proof

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;

then R_EAL ((F || E) . n) is E -measurable by A1, MESFUNC9:20;
hence (F || E) . n is E -measurable ; :: thesis: verum