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 & g is_simple_func_in S & f is nonnegative & g is nonnegative holds

( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (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 & g is_simple_func_in S & f is nonnegative & g is nonnegative holds

( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (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 & g is_simple_func_in S & f is nonnegative & g is nonnegative holds

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

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative implies ( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) ) )

assume that

A1: f is_simple_func_in S and

A2: g is_simple_func_in S and

A3: f is nonnegative and

A4: g is nonnegative ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) )

A5: g | (dom (f + g)) is nonnegative by A4, Th15;

A: f | (dom (f + g)) is nonnegative by A3, Th15;

not -infty in rng g by A4, Def3;

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

not -infty in rng f by A3, Def3;

then A8: f " {-infty} = {} by FUNCT_1:72;

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

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

A11: dom (f + g) is Element of S by A1, A2, Th37, Th38;

then A12: f | (dom (f + g)) is_simple_func_in S by A1, Th34;

A13: g | (dom (f + g)) is_simple_func_in S by A2, A11, Th34;

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 A10, XBOOLE_1:16;

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

then A15: dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) by A10, XBOOLE_1:16;

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative holds

( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (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 & g is_simple_func_in S & f is nonnegative & g is nonnegative holds

( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (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 & g is_simple_func_in S & f is nonnegative & g is nonnegative holds

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

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative implies ( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) ) )

assume that

A1: f is_simple_func_in S and

A2: g is_simple_func_in S and

A3: f is nonnegative and

A4: g is nonnegative ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) )

A5: g | (dom (f + g)) is nonnegative by A4, Th15;

A: f | (dom (f + g)) is nonnegative by A3, Th15;

not -infty in rng g by A4, Def3;

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

not -infty in rng f by A3, Def3;

then A8: f " {-infty} = {} by FUNCT_1:72;

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

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

A11: dom (f + g) is Element of S by A1, A2, Th37, Th38;

then A12: f | (dom (f + g)) is_simple_func_in S by A1, Th34;

A13: g | (dom (f + g)) is_simple_func_in S by A2, A11, Th34;

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 A10, XBOOLE_1:16;

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

then A15: dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) by A10, XBOOLE_1:16;

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

end;

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

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

then A17: integral' (M,(g | (dom (f + g)))) = 0 by A16, Def14;

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

then A18: integral' (M,(f | (dom (f + g)))) = 0 by A16, Def14;

integral' (M,(f + g)) = 0 by A16, Def14;

hence integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) by A18, A17; :: thesis: verum

end;then A17: integral' (M,(g | (dom (f + g)))) = 0 by A16, Def14;

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

then A18: integral' (M,(f | (dom (f + g)))) = 0 by A16, Def14;

integral' (M,(f + g)) = 0 by A16, Def14;

hence integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) by A18, A17; :: thesis: verum

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

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

.= {} by A7 ;

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

.= {} by A8 ;

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 A9, A14, A15, A20, MESFUNC1:def 3;

then A21: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = dom (f + g) by MESFUNC1:def 3;

A22: 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 A24: integral (M,(f + g)) = (integral (M,(f | (dom (f + g))))) + (integral (M,(g | (dom (f + g))))) by A21, A22, PARTFUN1:5;

A25: integral (M,(g | (dom (f + g)))) = integral' (M,(g | (dom (f + g)))) by A10, A15, A19, Def14;

integral (M,(f | (dom (f + g)))) = integral' (M,(f | (dom (f + g)))) by A10, A14, A19, Def14;

hence integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) by A19, A24, A25, Def14; :: thesis: verum

end;.= {} by A7 ;

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

.= {} by A8 ;

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 A9, A14, A15, A20, MESFUNC1:def 3;

then A21: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = dom (f + g) by MESFUNC1:def 3;

A22: 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))) + (g | (dom (f + g))))) = (integral (M,(f | (dom (f + g))))) + (integral (M,(g | (dom (f + g)))))
by A10, A12, A13, A14, A15, A19, MESFUNC4:5, A, A5;
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 A23: 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 3

.= (f . x) + ((g | (dom (f + g))) . x) by A21, A23, FUNCT_1:49

.= (f . x) + (g . x) by A21, A23, FUNCT_1:49 ;

hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A21, A23, MESFUNC1:def 3; :: thesis: verum

end;assume A23: 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 3

.= (f . x) + ((g | (dom (f + g))) . x) by A21, A23, FUNCT_1:49

.= (f . x) + (g . x) by A21, A23, FUNCT_1:49 ;

hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A21, A23, MESFUNC1:def 3; :: thesis: verum

then A24: integral (M,(f + g)) = (integral (M,(f | (dom (f + g))))) + (integral (M,(g | (dom (f + g))))) by A21, A22, PARTFUN1:5;

A25: integral (M,(g | (dom (f + g)))) = integral' (M,(g | (dom (f + g)))) by A10, A15, A19, Def14;

integral (M,(f | (dom (f + g)))) = integral' (M,(f | (dom (f + g)))) by A10, A14, A19, Def14;

hence integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) by A19, A24, A25, Def14; :: thesis: verum