let X be non empty set ; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL

for S being SigmaField of X

for E being Element of S

for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for S being SigmaField of X

for E being Element of S

for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let E be Element of S; :: thesis: for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let n be Nat; :: thesis: ( f . n is E -measurable implies (R_EAL f) . n is E -measurable )

assume f . n is E -measurable ; :: thesis: (R_EAL f) . n is E -measurable

then R_EAL (f . n) is E -measurable by MESFUNC6:def 1;

hence (R_EAL f) . n is E -measurable ; :: thesis: verum

for S being SigmaField of X

for E being Element of S

for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for S being SigmaField of X

for E being Element of S

for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let E be Element of S; :: thesis: for n being Nat st f . n is E -measurable holds

(R_EAL f) . n is E -measurable

let n be Nat; :: thesis: ( f . n is E -measurable implies (R_EAL f) . n is E -measurable )

assume f . n is E -measurable ; :: thesis: (R_EAL f) . n is E -measurable

then R_EAL (f . n) is E -measurable by MESFUNC6:def 1;

hence (R_EAL f) . n is E -measurable ; :: thesis: verum