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;

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

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;

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

proof

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;

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;
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;

end;