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 & g is_simple_func_in S ) and
A2: ( f is nonnegative & 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)))) )
( not -infty in rng f & not -infty in rng g ) by Def3, A2;
then A3: ( f " {-infty } = {} & g " {-infty } = {} ) by FUNCT_1:142;
then A4: ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) = (dom f) /\ (dom g) ;
hence A5: 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))))
dom (f + g) is Element of S by A1, Th43, Th44;
then A6: ( f | (dom (f + g)) is_simple_func_in S & g | (dom (f + g)) is_simple_func_in S ) by A1, Th40;
( f | (dom (f + g)) is nonnegative & g | (dom (f + g)) is nonnegative ) by A2, Th21;
then A7: for x being set holds
( ( x in dom (f | (dom (f + g))) implies 0 <= (f | (dom (f + g))) . x ) & ( x in dom (g | (dom (f + g))) implies 0 <= (g | (dom (f + g))) . x ) ) by SUPINF_2:70;
( dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) & dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) ) by RELAT_1:90;
then A8: ( dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) & dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) ) by A5, XBOOLE_1:16;

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

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

then A10: integral' M,(f + g) = 0 by Def14;
( dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) & dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) ) by RELAT_1:90;
then ( integral' M,(f | (dom (f + g))) = 0 & integral' M,(g | (dom (f + g))) = 0 ) by A9, Def14;
hence integral' M,(f + g) = (integral' M,(f | (dom (f + g)))) + (integral' M,(g | (dom (f + g)))) by A10; :: thesis: verum

end;

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

then A12: integral X,S,M,((f | (dom (f + g))) + (g | (dom (f + g)))) = (integral X,S,M,(f | (dom (f + g)))) + (integral X,S,M,(g | (dom (f + g)))) by A5, A6, A7, A8, MESFUNC4:5;
A13: (f | (dom (f + g))) " {-infty } = (dom (f + g)) /\ (f " {-infty }) by FUNCT_1:139
.= {} by A3 ;
(g | (dom (f + g))) " {-infty } = (dom (f + g)) /\ (g " {-infty }) by FUNCT_1:139
.= {} by A3 ;
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 A4, A8, A13, MESFUNC1:def 3;
then A14: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = dom (f + g) by MESFUNC1:def 3;
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 A15: 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 A14, A15, FUNCT_1:72
.= (f . x) + (g . x) by A14, A15, FUNCT_1:72 ;
hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A14, A15, MESFUNC1:def 3; :: thesis: verum

end;

then A16: integral X,S,M,(f + g) = (integral X,S,M,(f | (dom (f + g)))) + (integral X,S,M,(g | (dom (f + g)))) by A12, A14, PARTFUN1:34;
A17: integral X,S,M,(f | (dom (f + g))) = integral' M,(f | (dom (f + g))) by A5, A8, A11, Def14;
integral X,S,M,(g | (dom (f + g))) = integral' M,(g | (dom (f + g))) by A5, A8, A11, Def14;
hence integral' M,(f + g) = (integral' M,(f | (dom (f + g)))) + (integral' M,(g | (dom (f + g)))) by A11, A16, A17, Def14; :: thesis: verum

end;

end;