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