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,ExtREAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,f) & Integral (M,f) = integral' (M,f) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,f) & Integral (M,f) = integral' (M,f) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,f) & Integral (M,f) = integral' (M,f) )
let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & f is nonnegative implies ( Integral (M,f) = integral+ (M,f) & Integral (M,f) = integral' (M,f) ) )
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; :: thesis: ( Integral (M,f) = integral+ (M,f) & Integral (M,f) = integral' (M,f) )
reconsider A = dom f as Element of S by A1, Th37;
f is A -measurable by A1, MESFUNC2:34;
hence Integral (M,f) = integral+ (M,f) by A2, Th88; :: thesis: Integral (M,f) = integral' (M,f)
hence Integral (M,f) = integral' (M,f) by A1, A2, Th77; :: thesis: verum