let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let f be PartFunc of X,REAL; :: thesis: for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let A be Element of S; :: thesis: ( f is_simple_func_in S implies f is_measurable_on A )
assume f is_simple_func_in S ; :: thesis: f is_measurable_on A
then R_EAL f is_simple_func_in S by Th49;
then R_EAL f is_measurable_on A by MESFUNC2:34;
hence f is_measurable_on A by Def6; :: thesis: verum