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, Th21;
f | (dom (f + g)) is nonnegative by A3, Th21;
then A6: 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 A5, SUPINF_2:70;
not -infty in rng g by A4, Def3;
then A7: g " {-infty } = {} by FUNCT_1:142;
not -infty in rng f by A3, Def3;
then A8: f " {-infty } = {} by FUNCT_1:142;
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, Th43, Th44;
then A12: f | (dom (f + g)) is_simple_func_in S by A1, Th40;
A13: g | (dom (f + g)) is_simple_func_in S by A2, A11, Th40;
dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) by RELAT_1:90;
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:90;
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:90;
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:90;
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:139
.= {} by A7 ;
(f | (dom (f + g))) " {-infty } = (dom (f + g)) /\ (f " {-infty }) by FUNCT_1:139
.= {} 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:72
.= (f . x) + (g . x) by A21, A23, FUNCT_1:72 ;
hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A21, A23, MESFUNC1:def 3; :: thesis: verum

end;

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 A10, A12, A13, A6, A14, A15, A19, MESFUNC4:5;
then A24: integral X,S,M,(f + g) = (integral X,S,M,(f | (dom (f + g)))) + (integral X,S,M,(g | (dom (f + g)))) by A21, A22, PARTFUN1:34;
A25: integral X,S,M,(g | (dom (f + g))) = integral' M,(g | (dom (f + g))) by A10, A15, A19, Def14;
integral X,S,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;