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 set 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 set 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 set 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 set 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 set 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, Th21;
(- 1) (#) g is_simple_func_in S by A3, Th45;
then - g is_simple_func_in S by MESFUNC2:11;
then f + (- g) is_simple_func_in S by A1, Th44;
then f - g is_simple_func_in S by MESFUNC2:9;
then A7: dom (f - g) is Element of S by Th43;
then A8: g | (dom (f - g)) is_simple_func_in S by A3, Th40;
A9: g | (dom (f - g)) is nonnegative by A4, Th21;
g is without-infty by A3, Th20;
then not -infty in rng g by Def3;
then A10: g " {-infty } = {} by FUNCT_1:142;
f is without+infty by A1, Th20;
then not +infty in rng f by Def4;
then A11: f " {+infty } = {} by FUNCT_1:142;
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:90;
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

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:72;
hence (g | (dom (f - g))) . x <= (f | (dom (f - g))) . x by A13, A14, A16, FUNCT_1:72; :: thesis: verum

end;

dom (g | (dom (f - g))) = (dom g) /\ (dom (f - g)) by RELAT_1:90;
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, Th40;
thus integral' M,(f | (dom (f - g))) = (integral' M,(f - g)) + (integral' M,(g | (dom (f - g)))) :: thesis: verum

proof

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

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

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:139;
(f | (dom (f - g))) " {+infty } = (dom (f - g)) /\ (f " {+infty }) by FUNCT_1:139;
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

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:72
.= (f . x) - (g . x) by A24, A26, FUNCT_1:72 ;
hence ((f | (dom (f - g))) - (g | (dom (f - g)))) . x = (f - g) . x by A24, A26, MESFUNC1:def 4; :: thesis: verum

end;

integral X,S,M,(f | (dom (f - g))) = (integral X,S,M,((f | (dom (f - g))) - (g | (dom (f - g))))) + (integral X,S,M,(g | (dom (f - g)))) by A13, A18, A8, A6, A9, A14, A17, A15, A22, Lm9;
then A27: integral X,S,M,(f | (dom (f - g))) = (integral X,S,M,(f - g)) + (integral X,S,M,(g | (dom (f - g)))) by A24, A25, PARTFUN1:34;
A28: integral X,S,M,(g | (dom (f - g))) = integral' M,(g | (dom (f - g))) by A13, A17, A22, Def14;
integral X,S,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;

end;

end;