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 V61() & E = dom (f | E) & f | E is_measurable_on E & 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 V61() & E = dom (g | E) & g | E is_measurable_on E & 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_measurable_on E & (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 V61() & E = dom (f | E) & f | E is_measurable_on E & 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 V61() & E = dom (g | E) & g | E is_measurable_on E & 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_measurable_on E & (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 V61() & E = dom (f | E) & f | E is_measurable_on E & 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 V61() & E = dom (g | E) & g | E is_measurable_on E & 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_measurable_on E & (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 V61() & E = dom (f | E) & f | E is_measurable_on E & 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 V61() & E = dom (g | E) & g | E is_measurable_on E & 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_measurable_on E & (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 V61() & E = dom (f | E) & f | E is_measurable_on E & 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 V61() & E = dom (g | E) & g | E is_measurable_on E & 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_measurable_on E & (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, Th111;
reconsider NF = (f " {+infty }) \/ (f " {-infty }) as Element of S by A1, Th111;
set NFG = NF \/ NG;
consider E0 being Element of S such that
A5: E0 = dom f and
A6: f is_measurable_on E0 by A1, Def17;
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, Th113;
A8: (f " {-infty }) /\ (g " {+infty }) c= f " {-infty } by XBOOLE_1:17;
A9: for x being set 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 13;
then A10: g " {-infty } c= dom g by TARSKI:def 3;
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, XBOOLE_1:1;
f " {-infty } c= NF by XBOOLE_1:7;
then (f " {-infty }) /\ (g " {+infty }) c= NF by A8, XBOOLE_1:1;
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 Th35;
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, Th35;
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

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 set st x in dom g holds
g . x in ExtREAL ;
then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:5;
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:90;
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

assume (g | (E0 \ (NF \/ NG))) . x = -infty ; :: thesis: contradiction
then g . x = -infty by A20, FUNCT_1:70;
then gg . x in {-infty } by TARSKI:def 1;
then A25: x in gg " {-infty } by A22, FUNCT_2:46;
g " {-infty } c= NG by XBOOLE_1:7;
hence contradiction by A23, A25, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume (g | (E0 \ (NF \/ NG))) . x = +infty ; :: thesis: contradiction
then g . x = +infty by A20, FUNCT_1:70;
then gg . x in {+infty } by TARSKI:def 1;
then A26: x in gg " {+infty } by A22, FUNCT_2:46;
g " {+infty } c= NG by XBOOLE_1:7;
hence contradiction by A23, A26, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

then for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds
-infty < (g | (E0 \ (NF \/ NG))) . x ;
then A27: g | (E0 \ (NF \/ NG)) is without-infty by Th16;

now

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, EXTREAL2:59; :: thesis: verum

end;

then A31: g | (E0 \ (NF \/ NG)) is V61() by MESFUNC2:def 1;
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

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 set st x in dom f holds
f . x in ExtREAL ;
then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:5;
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:90;
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

assume (f | (E0 \ (NF \/ NG))) . x = -infty ; :: thesis: contradiction
then f . x = -infty by A33, FUNCT_1:70;
then ff . x in {-infty } by TARSKI:def 1;
then A38: x in ff " {-infty } by A35, FUNCT_2:46;
f " {-infty } c= NF by XBOOLE_1:7;
hence contradiction by A36, A38, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume (f | (E0 \ (NF \/ NG))) . x = +infty ; :: thesis: contradiction
then f . x = +infty by A33, FUNCT_1:70;
then ff . x in {+infty } by TARSKI:def 1;
then A39: x in ff " {+infty } by A35, FUNCT_2:46;
f " {+infty } c= NF by XBOOLE_1:7;
hence contradiction by A36, A39, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

then for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds
-infty < (f | (E0 \ (NF \/ NG))) . x ;
then A40: f | (E0 \ (NF \/ NG)) is without-infty by Th16;
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, Th30;
A42: (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is nonnegative by A40, A27, Th30;
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, Th30;
A44: (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG)))) is nonnegative by A40, A27, Th30;
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:90;
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_measurable_on Gf ) by A2, Def17;
then g is_measurable_on E0 \ (NF \/ NG) by A3, A5, MESFUNC1:34, XBOOLE_1:36;
then A51: g | (E0 \ (NF \/ NG)) is_measurable_on E0 \ (NF \/ NG) by A47, A48, Th48;
then A52: max- (g | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) by A48, MESFUNC2:28;
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:90;
then A57: E0 \ (NF \/ NG) = dom (f | (E0 \ (NF \/ NG))) by A5, XBOOLE_1:28, XBOOLE_1:36;
M . NG = 0 by A2, Th111;
then A58: NG is measure_zero of M by MEASURE1:def 13;
M . NF = 0 by A1, Th111;
then NF is measure_zero of M by MEASURE1:def 13;
then A59: NF \/ NG is measure_zero of M by A58, MEASURE1:70;
then A60: M . (NF \/ NG) = 0 by MEASURE1:def 13;
then A61: Integral M,f = Integral M,(f | (E0 \ (NF \/ NG))) by A5, A6, Th101;
E0 /\ (NF \/ NG) c= NF \/ NG by XBOOLE_1:17;
then DFPG \ (E0 \ (NF \/ NG)) is measure_zero of M by A59, A12, MEASURE1:69, XBOOLE_1:1;
then A62: M . (DFPG \ (E0 \ (NF \/ NG))) = 0 by MEASURE1:def 13;
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 without+infty by Th17;
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 without-infty by Th16;
A68: dom (max- (f | (E0 \ (NF \/ NG)))) = dom (f | (E0 \ (NF \/ NG))) by MESFUNC2:def 3;
A69: f " {-infty } c= dom f by A9, TARSKI:def 3;
g " {+infty } c= dom g by A9, TARSKI:def 3;
then A70: NG c= dom g by A10, XBOOLE_1:8;
f " {+infty } c= dom f by A9, TARSKI:def 3;
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, Th103;
then A74: 0 <= integral+ M,(max+ (g | (E0 \ (NF \/ NG)))) by Th102;
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 without+infty by Th17;
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 without-infty by Th16;
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, Th31;
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, Def17;
A80: 0 <= integral+ M,(max- (g | (E0 \ (NF \/ NG)))) by A73, Th102;
f is_measurable_on E0 \ (NF \/ NG) by A6, MESFUNC1:34, XBOOLE_1:36;
then A81: f | (E0 \ (NF \/ NG)) is_measurable_on E0 \ (NF \/ NG) by A56, A57, Th48;
then A82: max- (f | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) by A57, MESFUNC2:28;

now

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, EXTREAL2:59; :: thesis: verum

end;

then A86: f | (E0 \ (NF \/ NG)) is V61() by MESFUNC2:def 1;
then A87: (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) by A81, A51, A31, MESFUNC2:7;
then A88: max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is_measurable_on E0 \ (NF \/ NG) by MESFUNC2:27;
(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_measurable_on E0 \ (NF \/ NG) by A81, A51, A40, A27, Th50;
E0 \ (NF \/ NG) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) by A15, Th35;
then A90: max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is_measurable_on E0 \ (NF \/ NG) by A87, MESFUNC2:28;
A91: max+ (f | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) by A81, MESFUNC2:27;
A92: integral+ M,(max- (g | (E0 \ (NF \/ NG)))) <> +infty by A73, Def17;
(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is_measurable_on E0 \ (NF \/ NG) by A57, A81, A51, A40, A27, Th49;
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_measurable_on E0 \ (NF \/ NG) by A51, MESFUNC2:27;
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:31;
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:31;
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, Th103;
then A96: 0 <= integral+ M,(max+ (f | (E0 \ (NF \/ NG)))) by Th102;
A97: (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is_integrable_on M by A95, A73, Th114;
then A98: integral+ M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) <> +infty by Def17;
A99: integral+ M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) <> +infty by A97, Def17;
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, Th102;
A102: integral+ M,(max- (f | (E0 \ (NF \/ NG)))) <> +infty by A95, Def17;
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, Def17;
A105: 0 <= integral+ M,(max- (f | (E0 \ (NF \/ NG)))) by A95, Th102;
0 <= integral+ M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) by A97, Th102;
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:30;
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:30;
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:30;
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))))) = (R_EAL 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:30;
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:30;
then (R_EAL 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, Th101;
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 V61() & E = dom (f | E) & f | E is_measurable_on E & 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 V61() & E = dom (g | E) & g | E is_measurable_on E & 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_measurable_on E & (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, A81, A51, A86, A31, A87, A95, A73, A106, A61, Th114; :: thesis: verum