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

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

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

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) implies ( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) ) )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative and

A3: g is_simple_func_in S and

A4: g is nonnegative and

A5: for x being object st x in dom (f - g) holds

g . x <= f . x ; :: thesis: ( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

A6: f | (dom (f - g)) is nonnegative by A2, Th15;

(- jj) (#) g is_simple_func_in S by A3, Th39;

then - g is_simple_func_in S by MESFUNC2:9;

then f + (- g) is_simple_func_in S by A1, Th38;

then f - g is_simple_func_in S by MESFUNC2:8;

then A7: dom (f - g) is Element of S by Th37;

then A8: g | (dom (f - g)) is_simple_func_in S by A3, Th34;

A9: g | (dom (f - g)) is nonnegative by A4, Th15;

g is () by A3, Th14;

then not -infty in rng g ;

then A10: g " {-infty} = {} by FUNCT_1:72;

f is () by A1, Th14;

then not +infty in rng f ;

then A11: f " {+infty} = {} by FUNCT_1:72;

then A12: ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) = (dom f) /\ (dom g) by A10;

hence A13: dom (f - g) = (dom f) /\ (dom g) by MESFUNC1:def 4; :: thesis: integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g)))))

dom (f | (dom (f - g))) = (dom f) /\ (dom (f - g)) by RELAT_1:61;

then A14: dom (f | (dom (f - g))) = ((dom f) /\ (dom f)) /\ (dom g) by A13, XBOOLE_1:16;

A15: for x being set st x in dom (f | (dom (f - g))) holds

(g | (dom (f - g))) . x <= (f | (dom (f - g))) . x

then A17: dom (g | (dom (f - g))) = ((dom g) /\ (dom g)) /\ (dom f) by A13, XBOOLE_1:16;

A18: f | (dom (f - g)) is_simple_func_in S by A1, A7, Th34;

thus integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

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

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) implies ( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) ) )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative and

A3: g is_simple_func_in S and

A4: g is nonnegative and

A5: for x being object st x in dom (f - g) holds

g . x <= f . x ; :: thesis: ( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

A6: f | (dom (f - g)) is nonnegative by A2, Th15;

(- jj) (#) g is_simple_func_in S by A3, Th39;

then - g is_simple_func_in S by MESFUNC2:9;

then f + (- g) is_simple_func_in S by A1, Th38;

then f - g is_simple_func_in S by MESFUNC2:8;

then A7: dom (f - g) is Element of S by Th37;

then A8: g | (dom (f - g)) is_simple_func_in S by A3, Th34;

A9: g | (dom (f - g)) is nonnegative by A4, Th15;

g is () by A3, Th14;

then not -infty in rng g ;

then A10: g " {-infty} = {} by FUNCT_1:72;

f is () by A1, Th14;

then not +infty in rng f ;

then A11: f " {+infty} = {} by FUNCT_1:72;

then A12: ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) = (dom f) /\ (dom g) by A10;

hence A13: dom (f - g) = (dom f) /\ (dom g) by MESFUNC1:def 4; :: thesis: integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g)))))

dom (f | (dom (f - g))) = (dom f) /\ (dom (f - g)) by RELAT_1:61;

then A14: dom (f | (dom (f - g))) = ((dom f) /\ (dom f)) /\ (dom g) by A13, XBOOLE_1:16;

A15: for x being set st x in dom (f | (dom (f - g))) holds

(g | (dom (f - g))) . x <= (f | (dom (f - g))) . x

proof

dom (g | (dom (f - g))) = (dom g) /\ (dom (f - g))
by RELAT_1:61;
let x be set ; :: thesis: ( x in dom (f | (dom (f - g))) implies (g | (dom (f - g))) . x <= (f | (dom (f - g))) . x )

assume A16: x in dom (f | (dom (f - g))) ; :: thesis: (g | (dom (f - g))) . x <= (f | (dom (f - g))) . x

then g . x <= f . x by A5, A13, A14;

then (g | (dom (f - g))) . x <= f . x by A13, A14, A16, FUNCT_1:49;

hence (g | (dom (f - g))) . x <= (f | (dom (f - g))) . x by A13, A14, A16, FUNCT_1:49; :: thesis: verum

end;assume A16: x in dom (f | (dom (f - g))) ; :: thesis: (g | (dom (f - g))) . x <= (f | (dom (f - g))) . x

then g . x <= f . x by A5, A13, A14;

then (g | (dom (f - g))) . x <= f . x by A13, A14, A16, FUNCT_1:49;

hence (g | (dom (f - g))) . x <= (f | (dom (f - g))) . x by A13, A14, A16, FUNCT_1:49; :: thesis: verum

then A17: dom (g | (dom (f - g))) = ((dom g) /\ (dom g)) /\ (dom f) by A13, XBOOLE_1:16;

A18: f | (dom (f - g)) is_simple_func_in S by A1, A7, Th34;

thus integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) :: thesis: verum

proof
end;

per cases
( dom (f - g) = {} or dom (f - g) <> {} )
;

end;

suppose A19:
dom (f - g) = {}
; :: thesis: integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g)))))

dom (g | (dom (f - g))) = (dom g) /\ (dom (f - g))
by RELAT_1:61;

then A20: integral' (M,(g | (dom (f - g)))) = 0 by A19, Def14;

dom (f | (dom (f - g))) = (dom f) /\ (dom (f - g)) by RELAT_1:61;

then A21: integral' (M,(f | (dom (f - g)))) = 0 by A19, Def14;

integral' (M,(f - g)) = 0 by A19, Def14;

hence integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) by A21, A20; :: thesis: verum

end;then A20: integral' (M,(g | (dom (f - g)))) = 0 by A19, Def14;

dom (f | (dom (f - g))) = (dom f) /\ (dom (f - g)) by RELAT_1:61;

then A21: integral' (M,(f | (dom (f - g)))) = 0 by A19, Def14;

integral' (M,(f - g)) = 0 by A19, Def14;

hence integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) by A21, A20; :: thesis: verum

suppose A22:
dom (f - g) <> {}
; :: thesis: integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g)))))

A23:
(g | (dom (f - g))) " {-infty} = (dom (f - g)) /\ (g " {-infty})
by FUNCT_1:70;

(f | (dom (f - g))) " {+infty} = (dom (f - g)) /\ (f " {+infty}) by FUNCT_1:70;

then ((dom (f | (dom (f - g)))) /\ (dom (g | (dom (f - g))))) \ ((((f | (dom (f - g))) " {+infty}) /\ ((g | (dom (f - g))) " {+infty})) \/ (((f | (dom (f - g))) " {-infty}) /\ ((g | (dom (f - g))) " {-infty}))) = dom (f - g) by A11, A10, A12, A14, A17, A23, MESFUNC1:def 4;

then A24: dom ((f | (dom (f - g))) - (g | (dom (f - g)))) = dom (f - g) by MESFUNC1:def 4;

A25: for x being Element of X st x in dom ((f | (dom (f - g))) - (g | (dom (f - g)))) holds

((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x

then A27: integral (M,(f | (dom (f - g)))) = (integral (M,(f - g))) + (integral (M,(g | (dom (f - g))))) by A24, A25, PARTFUN1:5;

A28: integral (M,(g | (dom (f - g)))) = integral' (M,(g | (dom (f - g)))) by A13, A17, A22, Def14;

integral (M,(f | (dom (f - g)))) = integral' (M,(f | (dom (f - g)))) by A13, A14, A22, Def14;

hence integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) by A22, A27, A28, Def14; :: thesis: verum

end;(f | (dom (f - g))) " {+infty} = (dom (f - g)) /\ (f " {+infty}) by FUNCT_1:70;

then ((dom (f | (dom (f - g)))) /\ (dom (g | (dom (f - g))))) \ ((((f | (dom (f - g))) " {+infty}) /\ ((g | (dom (f - g))) " {+infty})) \/ (((f | (dom (f - g))) " {-infty}) /\ ((g | (dom (f - g))) " {-infty}))) = dom (f - g) by A11, A10, A12, A14, A17, A23, MESFUNC1:def 4;

then A24: dom ((f | (dom (f - g))) - (g | (dom (f - g)))) = dom (f - g) by MESFUNC1:def 4;

A25: for x being Element of X st x in dom ((f | (dom (f - g))) - (g | (dom (f - g)))) holds

((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x

proof

integral (M,(f | (dom (f - g)))) = (integral (M,((f | (dom (f - g))) - (g | (dom (f - g)))))) + (integral (M,(g | (dom (f - g)))))
by A13, A18, A8, A6, A9, A14, A17, A15, A22, Lm9;
let x be Element of X; :: thesis: ( x in dom ((f | (dom (f - g))) - (g | (dom (f - g)))) implies ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x )

assume A26: x in dom ((f | (dom (f - g))) - (g | (dom (f - g)))) ; :: thesis: ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x

then ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = ((f | (dom (f - g))) . x) - ((g | (dom (f - g))) . x) by MESFUNC1:def 4

.= (f . x) - ((g | (dom (f - g))) . x) by A24, A26, FUNCT_1:49

.= (f . x) - (g . x) by A24, A26, FUNCT_1:49 ;

hence ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x by A24, A26, MESFUNC1:def 4; :: thesis: verum

end;assume A26: x in dom ((f | (dom (f - g))) - (g | (dom (f - g)))) ; :: thesis: ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x

then ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = ((f | (dom (f - g))) . x) - ((g | (dom (f - g))) . x) by MESFUNC1:def 4

.= (f . x) - ((g | (dom (f - g))) . x) by A24, A26, FUNCT_1:49

.= (f . x) - (g . x) by A24, A26, FUNCT_1:49 ;

hence ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x by A24, A26, MESFUNC1:def 4; :: thesis: verum

then A27: integral (M,(f | (dom (f - g)))) = (integral (M,(f - g))) + (integral (M,(g | (dom (f - g))))) by A24, A25, PARTFUN1:5;

A28: integral (M,(g | (dom (f - g)))) = integral' (M,(g | (dom (f - g)))) by A13, A17, A22, Def14;

integral (M,(f | (dom (f - g)))) = integral' (M,(f | (dom (f - g)))) by A13, A14, A22, Def14;

hence integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) by A22, A27, A28, Def14; :: thesis: verum