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