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 ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

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 ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

Integral (M,f) = integral+ (M,f)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

Integral (M,f) = integral+ (M,f)

let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative implies Integral (M,f) = integral+ (M,f) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: f is nonnegative ; :: thesis: Integral (M,f) = integral+ (M,f)

A3: dom f = dom (max+ f) by MESFUNC2:def 2;

f = max+ f by A3, A4, FUNCT_1:2;

hence Integral (M,f) = (integral+ (M,f)) - 0 by A1, A7, A8, Th87, MESFUNC2:26

.= integral+ (M,f) by XXREAL_3:15 ;

:: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

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 ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

Integral (M,f) = integral+ (M,f)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

Integral (M,f) = integral+ (M,f)

let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative implies Integral (M,f) = integral+ (M,f) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: f is nonnegative ; :: thesis: Integral (M,f) = integral+ (M,f)

A3: dom f = dom (max+ f) by MESFUNC2:def 2;

A4: now :: thesis: for x being object st x in dom f holds

(max+ f) . x = f . x

A6:
dom f = dom (max- f)
by MESFUNC2:def 3;(max+ f) . x = f . x

let x be object ; :: thesis: ( x in dom f implies (max+ f) . x = f . x )

A5: 0 <= f . x by A2, SUPINF_2:51;

assume x in dom f ; :: thesis: (max+ f) . x = f . x

hence (max+ f) . x = max ((f . x),0) by A3, MESFUNC2:def 2

.= f . x by A5, XXREAL_0:def 10 ;

:: thesis: verum

end;A5: 0 <= f . x by A2, SUPINF_2:51;

assume x in dom f ; :: thesis: (max+ f) . x = f . x

hence (max+ f) . x = max ((f . x),0) by A3, MESFUNC2:def 2

.= f . x by A5, XXREAL_0:def 10 ;

:: thesis: verum

A7: now :: thesis: for x being Element of X st x in dom (max- f) holds

(max- f) . x = 0

A8:
dom f = dom (max- f)
by MESFUNC2:def 3;(max- f) . x = 0

let x be Element of X; :: thesis: ( x in dom (max- f) implies (max- f) . x = 0 )

assume x in dom (max- f) ; :: thesis: (max- f) . x = 0

then (max+ f) . x = f . x by A4, A6;

hence (max- f) . x = 0 by MESFUNC2:19; :: thesis: verum

end;assume x in dom (max- f) ; :: thesis: (max- f) . x = 0

then (max+ f) . x = f . x by A4, A6;

hence (max- f) . x = 0 by MESFUNC2:19; :: thesis: verum

f = max+ f by A3, A4, FUNCT_1:2;

hence Integral (M,f) = (integral+ (M,f)) - 0 by A1, A7, A8, Th87, MESFUNC2:26

.= integral+ (M,f) by XXREAL_3:15 ;

:: thesis: verum