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 natural number st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
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 natural number st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let S be SigmaField of X; :: thesis: for E being Element of S
for n being natural number st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let E be Element of S; :: thesis: for n being natural number st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let n be natural number ; :: thesis: ( f . n is_measurable_on E implies (R_EAL f) . n is_measurable_on E )
assume f . n is_measurable_on E ; :: thesis: (R_EAL f) . n is_measurable_on E
then R_EAL (f . n) is_measurable_on E by MESFUNC6:def 6;
hence (R_EAL f) . n is_measurable_on E ; :: thesis: verum