let X be non empty set ; 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; 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; 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; ( 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
; ( 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; Integral (M,f) = integral' (M,(R_EAL f))
hence
Integral (M,f) = integral' (M,(R_EAL f))
by A2, A3, MESFUNC5:77; verum