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_integrable_on M & g is_integrable_on M & dom f = dom g holds

ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

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_integrable_on M & g is_integrable_on M & dom f = dom g holds

ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds

ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M & g is_integrable_on M & dom f = dom g implies ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) )

assume that

A1: f is_integrable_on M and

A2: g is_integrable_on M and

A3: dom f = dom g ; :: thesis: ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

A4: (f " {+infty}) /\ (g " {-infty}) c= g " {-infty} by XBOOLE_1:17;

reconsider NG = (g " {+infty}) \/ (g " {-infty}) as Element of S by A2, Th105;

reconsider NF = (f " {+infty}) \/ (f " {-infty}) as Element of S by A1, Th105;

set NFG = NF \/ NG;

consider E0 being Element of S such that

A5: E0 = dom f and

A6: f is E0 -measurable by A1;

set E = E0 \ (NF \/ NG);

set f1 = f | (E0 \ (NF \/ NG));

set g1 = g | (E0 \ (NF \/ NG));

A7: E0 \ (NF \/ NG) c= dom f by A5, XBOOLE_1:36;

reconsider DFPG = dom (f + g) as Element of S by A1, A2, Th107;

A8: (f " {-infty}) /\ (g " {+infty}) c= f " {-infty} by XBOOLE_1:17;

A9: for x being object holds

( ( x in f " {+infty} implies x in dom f ) & ( x in f " {-infty} implies x in dom f ) & ( x in g " {+infty} implies x in dom g ) & ( x in g " {-infty} implies x in dom g ) ) by FUNCT_1:def 7;

then A10: g " {-infty} c= dom g ;

set NFPG = DFPG \ (E0 \ (NF \/ NG));

A11: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;

then DFPG \ (E0 \ (NF \/ NG)) c= E0 \ (E0 \ (NF \/ NG)) by A3, A5, XBOOLE_1:33, XBOOLE_1:36;

then A12: DFPG \ (E0 \ (NF \/ NG)) c= E0 /\ (NF \/ NG) by XBOOLE_1:48;

g " {-infty} c= NG by XBOOLE_1:7;

then A13: (f " {+infty}) /\ (g " {-infty}) c= NG by A4;

f " {-infty} c= NF by XBOOLE_1:7;

then (f " {-infty}) /\ (g " {+infty}) c= NF by A8;

then A14: ((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})) c= NF \/ NG by A13, XBOOLE_1:13;

then A15: E0 \ (NF \/ NG) c= dom (f + g) by A3, A5, A11, XBOOLE_1:34;

then A16: (f + g) | (E0 \ (NF \/ NG)) = (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) by Th29;

DFPG \ (DFPG \ (E0 \ (NF \/ NG))) = DFPG /\ (E0 \ (NF \/ NG)) by XBOOLE_1:48;

then A17: E0 \ (NF \/ NG) = DFPG \ (DFPG \ (E0 \ (NF \/ NG))) by A3, A5, A11, A14, XBOOLE_1:28, XBOOLE_1:34;

A18: dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by A15, Th29;

A19: for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds

( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty )

-infty < (g | (E0 \ (NF \/ NG))) . x ;

then A27: g | (E0 \ (NF \/ NG)) is () by Th10;

A32: for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds

( (f | (E0 \ (NF \/ NG))) . x < +infty & -infty < (f | (E0 \ (NF \/ NG))) . x )

-infty < (f | (E0 \ (NF \/ NG))) . x ;

then A40: f | (E0 \ (NF \/ NG)) is () by Th10;

then A41: dom ((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))) = (dom (f | (E0 \ (NF \/ NG)))) /\ (dom (g | (E0 \ (NF \/ NG)))) by A27, Th24;

A42: (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is nonnegative by A40, A27, Th24;

A43: dom ((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))) = (dom (f | (E0 \ (NF \/ NG)))) /\ (dom (g | (E0 \ (NF \/ NG)))) by A40, A27, Th24;

A44: (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG)))) is nonnegative by A40, A27, Th24;

A45: max+ (f | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A46: dom (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) by MESFUNC2:def 2;

A47: dom (g | (E0 \ (NF \/ NG))) = (dom g) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A48: E0 \ (NF \/ NG) = dom (g | (E0 \ (NF \/ NG))) by A3, A5, XBOOLE_1:28, XBOOLE_1:36;

then A49: dom (max- (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by MESFUNC2:def 3;

A50: ex Gf being Element of S st

( Gf = dom g & g is Gf -measurable ) by A2;

then g is E0 \ (NF \/ NG) -measurable by A3, A5, MESFUNC1:30, XBOOLE_1:36;

then A51: g | (E0 \ (NF \/ NG)) is E0 \ (NF \/ NG) -measurable by A47, A48, Th42;

then A52: max- (g | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A48, MESFUNC2:26;

A53: dom (max+ (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by A48, MESFUNC2:def 2;

A54: max+ (g | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A55: max- (g | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A56: dom (f | (E0 \ (NF \/ NG))) = (dom f) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A57: E0 \ (NF \/ NG) = dom (f | (E0 \ (NF \/ NG))) by A5, XBOOLE_1:28, XBOOLE_1:36;

M . NG = 0 by A2, Th105;

then A58: NG is measure_zero of M by MEASURE1:def 7;

M . NF = 0 by A1, Th105;

then NF is measure_zero of M by MEASURE1:def 7;

then A59: NF \/ NG is measure_zero of M by A58, MEASURE1:37;

then A60: M . (NF \/ NG) = 0 by MEASURE1:def 7;

then A61: Integral (M,f) = Integral (M,(f | (E0 \ (NF \/ NG)))) by A5, A6, Th95;

E0 /\ (NF \/ NG) c= NF \/ NG by XBOOLE_1:17;

then DFPG \ (E0 \ (NF \/ NG)) is measure_zero of M by A59, A12, MEASURE1:36, XBOOLE_1:1;

then A62: M . (DFPG \ (E0 \ (NF \/ NG))) = 0 by MEASURE1:def 7;

A63: max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is nonnegative by Lm1;

A64: max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is nonnegative by Lm1;

for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds

(g | (E0 \ (NF \/ NG))) . x < +infty by A19;

then A65: g | (E0 \ (NF \/ NG)) is () by Th11;

A66: dom (max+ (f | (E0 \ (NF \/ NG)))) = dom (f | (E0 \ (NF \/ NG))) by MESFUNC2:def 2;

for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds

-infty < (g | (E0 \ (NF \/ NG))) . x by A19;

then A67: g | (E0 \ (NF \/ NG)) is () by Th10;

A68: dom (max- (f | (E0 \ (NF \/ NG)))) = dom (f | (E0 \ (NF \/ NG))) by MESFUNC2:def 3;

A69: f " {-infty} c= dom f by A9;

g " {+infty} c= dom g by A9;

then A70: NG c= dom g by A10, XBOOLE_1:8;

f " {+infty} c= dom f by A9;

then NF c= dom g by A3, A69, XBOOLE_1:8;

then A71: NF \/ NG c= dom g by A70, XBOOLE_1:8;

A72: DFPG \ (E0 \ (NF \/ NG)) c= dom (f + g) by XBOOLE_1:36;

A73: g | (E0 \ (NF \/ NG)) is_integrable_on M by A2, Th97;

then A74: 0 <= integral+ (M,(max+ (g | (E0 \ (NF \/ NG))))) by Th96;

for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds

(f | (E0 \ (NF \/ NG))) . x < +infty by A32;

then A75: f | (E0 \ (NF \/ NG)) is () by Th11;

for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds

-infty < (f | (E0 \ (NF \/ NG))) . x by A32;

then f | (E0 \ (NF \/ NG)) is () by Th10;

then A76: ((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))) + (max- (g | (E0 \ (NF \/ NG)))) = ((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))) + (max+ (g | (E0 \ (NF \/ NG)))) by A75, A67, A65, Th25;

A77: max- (f | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A78: dom (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) by MESFUNC2:def 3;

A79: integral+ (M,(max+ (g | (E0 \ (NF \/ NG))))) <> +infty by A73;

A80: 0 <= integral+ (M,(max- (g | (E0 \ (NF \/ NG))))) by A73, Th96;

f is E0 \ (NF \/ NG) -measurable by A6, MESFUNC1:30, XBOOLE_1:36;

then A81: f | (E0 \ (NF \/ NG)) is E0 \ (NF \/ NG) -measurable by A56, A57, Th42;

then A82: max- (f | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A57, MESFUNC2:26;

then A87: (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A81, A51, A31, MESFUNC2:7;

then A88: max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by MESFUNC2:25;

(dom (f | (E0 \ (NF \/ NG)))) /\ (dom (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by A3, A5, A56, A47, XBOOLE_1:28, XBOOLE_1:36;

then A89: (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by A81, A51, A40, A27, Th44;

E0 \ (NF \/ NG) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) by A15, Th29;

then A90: max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by A87, MESFUNC2:26;

A91: max+ (f | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A81, MESFUNC2:25;

A92: integral+ (M,(max- (g | (E0 \ (NF \/ NG))))) <> +infty by A73;

(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by A57, A81, A51, A40, A27, Th43;

then A93: integral+ (M,(((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))) + (max- (g | (E0 \ (NF \/ NG)))))) = (integral+ (M,((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) by A57, A48, A43, A49, A42, A55, A52, Lm10

.= ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) by A18, A57, A68, A46, A77, A64, A88, A82, Lm10 ;

max+ (g | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A51, MESFUNC2:25;

then integral+ (M,(((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))) + (max+ (g | (E0 \ (NF \/ NG)))))) = (integral+ (M,((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) by A57, A48, A41, A53, A44, A54, A89, Lm10

.= ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) by A18, A57, A66, A78, A45, A63, A90, A91, Lm10 ;

then ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) = (((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (g | (E0 \ (NF \/ NG))))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) by A76, A80, A92, A93, XXREAL_3:30;

then ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) = ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by A74, A79, A80, A92, XXREAL_3:30;

then ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + 0. = ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:7;

then A94: (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:4;

A95: f | (E0 \ (NF \/ NG)) is_integrable_on M by A1, Th97;

then A96: 0 <= integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))) by Th96;

A97: (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is_integrable_on M by A95, A73, Th108;

then A98: integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) <> +infty ;

A99: integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) <> +infty by A97;

then A100: - (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) <> -infty by XXREAL_3:23;

A101: 0 <= integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) by A97, Th96;

A102: integral+ (M,(max- (f | (E0 \ (NF \/ NG))))) <> +infty by A95;

then A103: - (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) <> -infty by XXREAL_3:23;

A104: integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))) <> +infty by A95;

A105: 0 <= integral+ (M,(max- (f | (E0 \ (NF \/ NG))))) by A95, Th96;

0 <= integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) by A97, Th96;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = (- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by A105, A102, A98, A94, XXREAL_3:29;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = (- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))))) by A96, A104, A101, A99, XXREAL_3:29;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by A101, A99, A100, XXREAL_3:29;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = 0 + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by XXREAL_3:7;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = (integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:4;

then ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) = (- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by A105, A102, A103, XXREAL_3:29;

then ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) = ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by A96, A104, A105, A103, XXREAL_3:29;

then 0 + ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) = ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:7;

then A106: Integral (M,((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = (Integral (M,(f | (E0 \ (NF \/ NG))))) + (Integral (M,(g | (E0 \ (NF \/ NG))))) by XXREAL_3:4;

Integral (M,g) = Integral (M,(g | (E0 \ (NF \/ NG)))) by A3, A5, A50, A60, Th95;

hence ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by A3, A5, A60, A71, A15, A16, A18, A62, A17, A72, A7, A57, A48, A86, A31, A87, A95, A73, A106, A61, Th108; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds

ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

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_integrable_on M & g is_integrable_on M & dom f = dom g holds

ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds

ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M & g is_integrable_on M & dom f = dom g implies ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) )

assume that

A1: f is_integrable_on M and

A2: g is_integrable_on M and

A3: dom f = dom g ; :: thesis: ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

A4: (f " {+infty}) /\ (g " {-infty}) c= g " {-infty} by XBOOLE_1:17;

reconsider NG = (g " {+infty}) \/ (g " {-infty}) as Element of S by A2, Th105;

reconsider NF = (f " {+infty}) \/ (f " {-infty}) as Element of S by A1, Th105;

set NFG = NF \/ NG;

consider E0 being Element of S such that

A5: E0 = dom f and

A6: f is E0 -measurable by A1;

set E = E0 \ (NF \/ NG);

set f1 = f | (E0 \ (NF \/ NG));

set g1 = g | (E0 \ (NF \/ NG));

A7: E0 \ (NF \/ NG) c= dom f by A5, XBOOLE_1:36;

reconsider DFPG = dom (f + g) as Element of S by A1, A2, Th107;

A8: (f " {-infty}) /\ (g " {+infty}) c= f " {-infty} by XBOOLE_1:17;

A9: for x being object holds

( ( x in f " {+infty} implies x in dom f ) & ( x in f " {-infty} implies x in dom f ) & ( x in g " {+infty} implies x in dom g ) & ( x in g " {-infty} implies x in dom g ) ) by FUNCT_1:def 7;

then A10: g " {-infty} c= dom g ;

set NFPG = DFPG \ (E0 \ (NF \/ NG));

A11: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;

then DFPG \ (E0 \ (NF \/ NG)) c= E0 \ (E0 \ (NF \/ NG)) by A3, A5, XBOOLE_1:33, XBOOLE_1:36;

then A12: DFPG \ (E0 \ (NF \/ NG)) c= E0 /\ (NF \/ NG) by XBOOLE_1:48;

g " {-infty} c= NG by XBOOLE_1:7;

then A13: (f " {+infty}) /\ (g " {-infty}) c= NG by A4;

f " {-infty} c= NF by XBOOLE_1:7;

then (f " {-infty}) /\ (g " {+infty}) c= NF by A8;

then A14: ((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})) c= NF \/ NG by A13, XBOOLE_1:13;

then A15: E0 \ (NF \/ NG) c= dom (f + g) by A3, A5, A11, XBOOLE_1:34;

then A16: (f + g) | (E0 \ (NF \/ NG)) = (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) by Th29;

DFPG \ (DFPG \ (E0 \ (NF \/ NG))) = DFPG /\ (E0 \ (NF \/ NG)) by XBOOLE_1:48;

then A17: E0 \ (NF \/ NG) = DFPG \ (DFPG \ (E0 \ (NF \/ NG))) by A3, A5, A11, A14, XBOOLE_1:28, XBOOLE_1:34;

A18: dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by A15, Th29;

A19: for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds

( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty )

proof

then
for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds
let x be set ; :: thesis: ( x in dom (g | (E0 \ (NF \/ NG))) implies ( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty ) )

for x being object st x in dom g holds

g . x in ExtREAL by XXREAL_0:def 1;

then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:3;

assume A20: x in dom (g | (E0 \ (NF \/ NG))) ; :: thesis: ( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty )

then A21: x in (dom g) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A22: x in dom g by XBOOLE_0:def 4;

x in E0 \ (NF \/ NG) by A21, XBOOLE_0:def 4;

then A23: not x in NF \/ NG by XBOOLE_0:def 5;

end;for x being object st x in dom g holds

g . x in ExtREAL by XXREAL_0:def 1;

then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:3;

assume A20: x in dom (g | (E0 \ (NF \/ NG))) ; :: thesis: ( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty )

then A21: x in (dom g) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A22: x in dom g by XBOOLE_0:def 4;

x in E0 \ (NF \/ NG) by A21, XBOOLE_0:def 4;

then A23: not x in NF \/ NG by XBOOLE_0:def 5;

A24: now :: thesis: not (g | (E0 \ (NF \/ NG))) . x = -infty

assume
(g | (E0 \ (NF \/ NG))) . x = -infty
; :: thesis: contradiction

then g . x = -infty by A20, FUNCT_1:47;

then gg . x in {-infty} by TARSKI:def 1;

then A25: x in gg " {-infty} by A22, FUNCT_2:38;

g " {-infty} c= NG by XBOOLE_1:7;

hence contradiction by A23, A25, XBOOLE_0:def 3; :: thesis: verum

end;then g . x = -infty by A20, FUNCT_1:47;

then gg . x in {-infty} by TARSKI:def 1;

then A25: x in gg " {-infty} by A22, FUNCT_2:38;

g " {-infty} c= NG by XBOOLE_1:7;

hence contradiction by A23, A25, XBOOLE_0:def 3; :: thesis: verum

now :: thesis: not (g | (E0 \ (NF \/ NG))) . x = +infty

hence
( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty )
by A24, XXREAL_0:4, XXREAL_0:6; :: thesis: verumassume
(g | (E0 \ (NF \/ NG))) . x = +infty
; :: thesis: contradiction

then g . x = +infty by A20, FUNCT_1:47;

then gg . x in {+infty} by TARSKI:def 1;

then A26: x in gg " {+infty} by A22, FUNCT_2:38;

g " {+infty} c= NG by XBOOLE_1:7;

hence contradiction by A23, A26, XBOOLE_0:def 3; :: thesis: verum

end;then g . x = +infty by A20, FUNCT_1:47;

then gg . x in {+infty} by TARSKI:def 1;

then A26: x in gg " {+infty} by A22, FUNCT_2:38;

g " {+infty} c= NG by XBOOLE_1:7;

hence contradiction by A23, A26, XBOOLE_0:def 3; :: thesis: verum

-infty < (g | (E0 \ (NF \/ NG))) . x ;

then A27: g | (E0 \ (NF \/ NG)) is () by Th10;

now :: thesis: for x being Element of X st x in dom (g | (E0 \ (NF \/ NG))) holds

|.((g | (E0 \ (NF \/ NG))) . x).| < +infty

then A31:
g | (E0 \ (NF \/ NG)) is real-valued
by MESFUNC2:def 1;|.((g | (E0 \ (NF \/ NG))) . x).| < +infty

let x be Element of X; :: thesis: ( x in dom (g | (E0 \ (NF \/ NG))) implies |.((g | (E0 \ (NF \/ NG))) . x).| < +infty )

A28: - +infty = -infty by XXREAL_3:def 3;

assume A29: x in dom (g | (E0 \ (NF \/ NG))) ; :: thesis: |.((g | (E0 \ (NF \/ NG))) . x).| < +infty

then A30: (g | (E0 \ (NF \/ NG))) . x < +infty by A19;

-infty < (g | (E0 \ (NF \/ NG))) . x by A19, A29;

hence |.((g | (E0 \ (NF \/ NG))) . x).| < +infty by A30, A28, EXTREAL1:22; :: thesis: verum

end;A28: - +infty = -infty by XXREAL_3:def 3;

assume A29: x in dom (g | (E0 \ (NF \/ NG))) ; :: thesis: |.((g | (E0 \ (NF \/ NG))) . x).| < +infty

then A30: (g | (E0 \ (NF \/ NG))) . x < +infty by A19;

-infty < (g | (E0 \ (NF \/ NG))) . x by A19, A29;

hence |.((g | (E0 \ (NF \/ NG))) . x).| < +infty by A30, A28, EXTREAL1:22; :: thesis: verum

A32: for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds

( (f | (E0 \ (NF \/ NG))) . x < +infty & -infty < (f | (E0 \ (NF \/ NG))) . x )

proof

then
for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds
let x be set ; :: thesis: ( x in dom (f | (E0 \ (NF \/ NG))) implies ( (f | (E0 \ (NF \/ NG))) . x < +infty & -infty < (f | (E0 \ (NF \/ NG))) . x ) )

for x being object st x in dom f holds

f . x in ExtREAL by XXREAL_0:def 1;

then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:3;

assume A33: x in dom (f | (E0 \ (NF \/ NG))) ; :: thesis: ( (f | (E0 \ (NF \/ NG))) . x < +infty & -infty < (f | (E0 \ (NF \/ NG))) . x )

then A34: x in (dom f) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A35: x in dom f by XBOOLE_0:def 4;

x in E0 \ (NF \/ NG) by A34, XBOOLE_0:def 4;

then A36: not x in NF \/ NG by XBOOLE_0:def 5;

end;for x being object st x in dom f holds

f . x in ExtREAL by XXREAL_0:def 1;

then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:3;

assume A33: x in dom (f | (E0 \ (NF \/ NG))) ; :: thesis: ( (f | (E0 \ (NF \/ NG))) . x < +infty & -infty < (f | (E0 \ (NF \/ NG))) . x )

then A34: x in (dom f) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A35: x in dom f by XBOOLE_0:def 4;

x in E0 \ (NF \/ NG) by A34, XBOOLE_0:def 4;

then A36: not x in NF \/ NG by XBOOLE_0:def 5;

A37: now :: thesis: not (f | (E0 \ (NF \/ NG))) . x = -infty

assume
(f | (E0 \ (NF \/ NG))) . x = -infty
; :: thesis: contradiction

then f . x = -infty by A33, FUNCT_1:47;

then ff . x in {-infty} by TARSKI:def 1;

then A38: x in ff " {-infty} by A35, FUNCT_2:38;

f " {-infty} c= NF by XBOOLE_1:7;

hence contradiction by A36, A38, XBOOLE_0:def 3; :: thesis: verum

end;then f . x = -infty by A33, FUNCT_1:47;

then ff . x in {-infty} by TARSKI:def 1;

then A38: x in ff " {-infty} by A35, FUNCT_2:38;

f " {-infty} c= NF by XBOOLE_1:7;

hence contradiction by A36, A38, XBOOLE_0:def 3; :: thesis: verum

now :: thesis: not (f | (E0 \ (NF \/ NG))) . x = +infty

hence
( (f | (E0 \ (NF \/ NG))) . x < +infty & -infty < (f | (E0 \ (NF \/ NG))) . x )
by A37, XXREAL_0:4, XXREAL_0:6; :: thesis: verumassume
(f | (E0 \ (NF \/ NG))) . x = +infty
; :: thesis: contradiction

then f . x = +infty by A33, FUNCT_1:47;

then ff . x in {+infty} by TARSKI:def 1;

then A39: x in ff " {+infty} by A35, FUNCT_2:38;

f " {+infty} c= NF by XBOOLE_1:7;

hence contradiction by A36, A39, XBOOLE_0:def 3; :: thesis: verum

end;then f . x = +infty by A33, FUNCT_1:47;

then ff . x in {+infty} by TARSKI:def 1;

then A39: x in ff " {+infty} by A35, FUNCT_2:38;

f " {+infty} c= NF by XBOOLE_1:7;

hence contradiction by A36, A39, XBOOLE_0:def 3; :: thesis: verum

-infty < (f | (E0 \ (NF \/ NG))) . x ;

then A40: f | (E0 \ (NF \/ NG)) is () by Th10;

then A41: dom ((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))) = (dom (f | (E0 \ (NF \/ NG)))) /\ (dom (g | (E0 \ (NF \/ NG)))) by A27, Th24;

A42: (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is nonnegative by A40, A27, Th24;

A43: dom ((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))) = (dom (f | (E0 \ (NF \/ NG)))) /\ (dom (g | (E0 \ (NF \/ NG)))) by A40, A27, Th24;

A44: (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG)))) is nonnegative by A40, A27, Th24;

A45: max+ (f | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A46: dom (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) by MESFUNC2:def 2;

A47: dom (g | (E0 \ (NF \/ NG))) = (dom g) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A48: E0 \ (NF \/ NG) = dom (g | (E0 \ (NF \/ NG))) by A3, A5, XBOOLE_1:28, XBOOLE_1:36;

then A49: dom (max- (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by MESFUNC2:def 3;

A50: ex Gf being Element of S st

( Gf = dom g & g is Gf -measurable ) by A2;

then g is E0 \ (NF \/ NG) -measurable by A3, A5, MESFUNC1:30, XBOOLE_1:36;

then A51: g | (E0 \ (NF \/ NG)) is E0 \ (NF \/ NG) -measurable by A47, A48, Th42;

then A52: max- (g | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A48, MESFUNC2:26;

A53: dom (max+ (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by A48, MESFUNC2:def 2;

A54: max+ (g | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A55: max- (g | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A56: dom (f | (E0 \ (NF \/ NG))) = (dom f) /\ (E0 \ (NF \/ NG)) by RELAT_1:61;

then A57: E0 \ (NF \/ NG) = dom (f | (E0 \ (NF \/ NG))) by A5, XBOOLE_1:28, XBOOLE_1:36;

M . NG = 0 by A2, Th105;

then A58: NG is measure_zero of M by MEASURE1:def 7;

M . NF = 0 by A1, Th105;

then NF is measure_zero of M by MEASURE1:def 7;

then A59: NF \/ NG is measure_zero of M by A58, MEASURE1:37;

then A60: M . (NF \/ NG) = 0 by MEASURE1:def 7;

then A61: Integral (M,f) = Integral (M,(f | (E0 \ (NF \/ NG)))) by A5, A6, Th95;

E0 /\ (NF \/ NG) c= NF \/ NG by XBOOLE_1:17;

then DFPG \ (E0 \ (NF \/ NG)) is measure_zero of M by A59, A12, MEASURE1:36, XBOOLE_1:1;

then A62: M . (DFPG \ (E0 \ (NF \/ NG))) = 0 by MEASURE1:def 7;

A63: max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is nonnegative by Lm1;

A64: max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is nonnegative by Lm1;

for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds

(g | (E0 \ (NF \/ NG))) . x < +infty by A19;

then A65: g | (E0 \ (NF \/ NG)) is () by Th11;

A66: dom (max+ (f | (E0 \ (NF \/ NG)))) = dom (f | (E0 \ (NF \/ NG))) by MESFUNC2:def 2;

for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds

-infty < (g | (E0 \ (NF \/ NG))) . x by A19;

then A67: g | (E0 \ (NF \/ NG)) is () by Th10;

A68: dom (max- (f | (E0 \ (NF \/ NG)))) = dom (f | (E0 \ (NF \/ NG))) by MESFUNC2:def 3;

A69: f " {-infty} c= dom f by A9;

g " {+infty} c= dom g by A9;

then A70: NG c= dom g by A10, XBOOLE_1:8;

f " {+infty} c= dom f by A9;

then NF c= dom g by A3, A69, XBOOLE_1:8;

then A71: NF \/ NG c= dom g by A70, XBOOLE_1:8;

A72: DFPG \ (E0 \ (NF \/ NG)) c= dom (f + g) by XBOOLE_1:36;

A73: g | (E0 \ (NF \/ NG)) is_integrable_on M by A2, Th97;

then A74: 0 <= integral+ (M,(max+ (g | (E0 \ (NF \/ NG))))) by Th96;

for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds

(f | (E0 \ (NF \/ NG))) . x < +infty by A32;

then A75: f | (E0 \ (NF \/ NG)) is () by Th11;

for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds

-infty < (f | (E0 \ (NF \/ NG))) . x by A32;

then f | (E0 \ (NF \/ NG)) is () by Th10;

then A76: ((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))) + (max- (g | (E0 \ (NF \/ NG)))) = ((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))) + (max+ (g | (E0 \ (NF \/ NG)))) by A75, A67, A65, Th25;

A77: max- (f | (E0 \ (NF \/ NG))) is nonnegative by Lm1;

A78: dom (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) by MESFUNC2:def 3;

A79: integral+ (M,(max+ (g | (E0 \ (NF \/ NG))))) <> +infty by A73;

A80: 0 <= integral+ (M,(max- (g | (E0 \ (NF \/ NG))))) by A73, Th96;

f is E0 \ (NF \/ NG) -measurable by A6, MESFUNC1:30, XBOOLE_1:36;

then A81: f | (E0 \ (NF \/ NG)) is E0 \ (NF \/ NG) -measurable by A56, A57, Th42;

then A82: max- (f | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A57, MESFUNC2:26;

now :: thesis: for x being Element of X st x in dom (f | (E0 \ (NF \/ NG))) holds

|.((f | (E0 \ (NF \/ NG))) . x).| < +infty

then A86:
f | (E0 \ (NF \/ NG)) is real-valued
by MESFUNC2:def 1;|.((f | (E0 \ (NF \/ NG))) . x).| < +infty

let x be Element of X; :: thesis: ( x in dom (f | (E0 \ (NF \/ NG))) implies |.((f | (E0 \ (NF \/ NG))) . x).| < +infty )

A83: - +infty = -infty by XXREAL_3:def 3;

assume A84: x in dom (f | (E0 \ (NF \/ NG))) ; :: thesis: |.((f | (E0 \ (NF \/ NG))) . x).| < +infty

then A85: (f | (E0 \ (NF \/ NG))) . x < +infty by A32;

-infty < (f | (E0 \ (NF \/ NG))) . x by A32, A84;

hence |.((f | (E0 \ (NF \/ NG))) . x).| < +infty by A85, A83, EXTREAL1:22; :: thesis: verum

end;A83: - +infty = -infty by XXREAL_3:def 3;

assume A84: x in dom (f | (E0 \ (NF \/ NG))) ; :: thesis: |.((f | (E0 \ (NF \/ NG))) . x).| < +infty

then A85: (f | (E0 \ (NF \/ NG))) . x < +infty by A32;

-infty < (f | (E0 \ (NF \/ NG))) . x by A32, A84;

hence |.((f | (E0 \ (NF \/ NG))) . x).| < +infty by A85, A83, EXTREAL1:22; :: thesis: verum

then A87: (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A81, A51, A31, MESFUNC2:7;

then A88: max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by MESFUNC2:25;

(dom (f | (E0 \ (NF \/ NG)))) /\ (dom (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by A3, A5, A56, A47, XBOOLE_1:28, XBOOLE_1:36;

then A89: (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by A81, A51, A40, A27, Th44;

E0 \ (NF \/ NG) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) by A15, Th29;

then A90: max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by A87, MESFUNC2:26;

A91: max+ (f | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A81, MESFUNC2:25;

A92: integral+ (M,(max- (g | (E0 \ (NF \/ NG))))) <> +infty by A73;

(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is E0 \ (NF \/ NG) -measurable by A57, A81, A51, A40, A27, Th43;

then A93: integral+ (M,(((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))) + (max- (g | (E0 \ (NF \/ NG)))))) = (integral+ (M,((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) by A57, A48, A43, A49, A42, A55, A52, Lm10

.= ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) by A18, A57, A68, A46, A77, A64, A88, A82, Lm10 ;

max+ (g | (E0 \ (NF \/ NG))) is E0 \ (NF \/ NG) -measurable by A51, MESFUNC2:25;

then integral+ (M,(((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))) + (max+ (g | (E0 \ (NF \/ NG)))))) = (integral+ (M,((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) by A57, A48, A41, A53, A44, A54, A89, Lm10

.= ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) by A18, A57, A66, A78, A45, A63, A90, A91, Lm10 ;

then ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) = (((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (g | (E0 \ (NF \/ NG))))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) by A76, A80, A92, A93, XXREAL_3:30;

then ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) = ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by A74, A79, A80, A92, XXREAL_3:30;

then ((integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + 0. = ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:7;

then A94: (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:4;

A95: f | (E0 \ (NF \/ NG)) is_integrable_on M by A1, Th97;

then A96: 0 <= integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))) by Th96;

A97: (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is_integrable_on M by A95, A73, Th108;

then A98: integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) <> +infty ;

A99: integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) <> +infty by A97;

then A100: - (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) <> -infty by XXREAL_3:23;

A101: 0 <= integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) by A97, Th96;

A102: integral+ (M,(max- (f | (E0 \ (NF \/ NG))))) <> +infty by A95;

then A103: - (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) <> -infty by XXREAL_3:23;

A104: integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))) <> +infty by A95;

A105: 0 <= integral+ (M,(max- (f | (E0 \ (NF \/ NG))))) by A95, Th96;

0 <= integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) by A97, Th96;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = (- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by A105, A102, A98, A94, XXREAL_3:29;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = (- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + ((integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))))) by A96, A104, A101, A99, XXREAL_3:29;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by A101, A99, A100, XXREAL_3:29;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = 0 + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by XXREAL_3:7;

then ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG)))))) = (integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:4;

then ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) = (- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (f | (E0 \ (NF \/ NG)))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG)))))))) by A105, A102, A103, XXREAL_3:29;

then ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) = ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by A96, A104, A105, A103, XXREAL_3:29;

then 0 + ((- (integral+ (M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) + (integral+ (M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))))) = ((- (integral+ (M,(max- (f | (E0 \ (NF \/ NG))))))) + (integral+ (M,(max+ (f | (E0 \ (NF \/ NG))))))) + ((integral+ (M,(max+ (g | (E0 \ (NF \/ NG)))))) - (integral+ (M,(max- (g | (E0 \ (NF \/ NG))))))) by XXREAL_3:7;

then A106: Integral (M,((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = (Integral (M,(f | (E0 \ (NF \/ NG))))) + (Integral (M,(g | (E0 \ (NF \/ NG))))) by XXREAL_3:4;

Integral (M,g) = Integral (M,(g | (E0 \ (NF \/ NG)))) by A3, A5, A50, A60, Th95;

hence ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by A3, A5, A60, A71, A15, A16, A18, A62, A17, A72, A7, A57, A48, A86, A31, A87, A95, A73, A106, A61, Th108; :: thesis: verum