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_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 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_measurable_on E ) holds
(F || E) . n is_measurable_on E
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_measurable_on E ) holds
(F || E) . n is_measurable_on E
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_measurable_on E ) holds
(F || E) . n is_measurable_on E
let n be Nat; :: 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 A1: ( F is with_the_same_dom & 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 )
assume A2: for m being Nat holds F . m is_measurable_on E ; :: thesis: (F || E) . n is_measurable_on E
for m being Nat holds
( (R_EAL F) . m is_measurable_on E & (R_EAL (F || E)) . m = ((R_EAL F) . m) | E )

proof

let m be Nat; :: thesis: ( (R_EAL F) . m is_measurable_on E & (R_EAL (F || E)) . m = ((R_EAL F) . m) | E )
F . m is_measurable_on E by A2;
then R_EAL (F . m) is_measurable_on E by MESFUNC6:def 6;
hence (R_EAL F) . m is_measurable_on E ; :: 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_measurable_on E by A1, MESFUNC9:20;
hence (F || E) . n is_measurable_on E by MESFUNC6:def 6; :: thesis: verum