let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
let f be PartFunc of X,REAL; :: thesis: ( f is_simple_func_in S & f is nonnegative implies ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) )
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; :: thesis: ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
A3: R_EAL f is_simple_func_in S by A1, Th49;
then reconsider A = dom (R_EAL f) as Element of S by MESFUNC5:37;
R_EAL f is A -measurable by A3, MESFUNC2:34;
then f is A -measurable ;
hence Integral (M,f) = integral+ (M,(R_EAL f)) by A2, Th82; :: thesis: Integral (M,f) = integral' (M,(R_EAL f))
hence Integral (M,f) = integral' (M,(R_EAL f)) by A2, A3, MESFUNC5:77; :: thesis: verum