let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

let M be sigma_Measure of S; :: thesis: for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

let f be nonnegative PartFunc of X,ExtREAL; :: thesis: integral' (M,(max- (- f))) = integral' (M,f)

- f = - (max- (- f)) by Th32;

then f = - (- (max- (- f))) by Th36;

then f = (- 1) (#) (- (max- (- f))) by MESFUNC2:9;

then f = (- 1) (#) ((- 1) (#) (max- (- f))) by MESFUNC2:9;

then f = ((- 1) * (- 1)) (#) (max- (- f)) by Th35;

hence integral' (M,(max- (- f))) = integral' (M,f) by MESFUNC2:1; :: thesis: verum

for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

let M be sigma_Measure of S; :: thesis: for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

let f be nonnegative PartFunc of X,ExtREAL; :: thesis: integral' (M,(max- (- f))) = integral' (M,f)

- f = - (max- (- f)) by Th32;

then f = - (- (max- (- f))) by Th36;

then f = (- 1) (#) (- (max- (- f))) by MESFUNC2:9;

then f = (- 1) (#) ((- 1) (#) (max- (- f))) by MESFUNC2:9;

then f = ((- 1) * (- 1)) (#) (max- (- f)) by Th35;

hence integral' (M,(max- (- f))) = integral' (M,f) by MESFUNC2:1; :: thesis: verum