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

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