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_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 real-valued & 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 real-valued & 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 real-valued & 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 real-valued & 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 real-valued & 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 real-valued & 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 real-valued & 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 A1: ( f is_integrable_on M & g is_integrable_on M & 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_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 real-valued & 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)) )
consider E0 being Element of S such that
A2: ( E0 = dom f & f is_measurable_on E0 ) by A1, Def17;
A3: ex Gf being Element of S st
( Gf = dom g & g is_measurable_on Gf ) by A1, Def17;
reconsider NF = (f " {+infty }) \/ (f " {-infty }) as Element of S by A1, Th111;
reconsider NG = (g " {+infty }) \/ (g " {-infty }) as Element of S by A1, Th111;
set NFG = NF \/ NG;
( M . NF = 0 & M . NG = 0 ) by A1, Th111;
then ( NF is measure_zero of M & NG is measure_zero of M ) by MEASURE1:def 13;
then A4: NF \/ NG is measure_zero of M by MEASURE1:70;
then A5: M . (NF \/ NG) = 0 by MEASURE1:def 13;
set E = E0 \ (NF \/ NG);
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 ( f " {+infty } c= dom f & f " {-infty } c= dom f & g " {+infty } c= dom g & g " {-infty } c= dom g ) by TARSKI:def 3;
then ( NF c= dom g & NG c= dom g ) by A1, XBOOLE_1:8;
then A6: NF \/ NG c= dom g by XBOOLE_1:8;
A7: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
set f1 = f | (E0 \ (NF \/ NG));
set g1 = g | (E0 \ (NF \/ NG));
( f " {-infty } c= NF & g " {-infty } c= NG & (f " {-infty }) /\ (g " {+infty }) c= f " {-infty } & (f " {+infty }) /\ (g " {-infty }) c= g " {-infty } ) by XBOOLE_1:7, XBOOLE_1:17;
then ( (f " {-infty }) /\ (g " {+infty }) c= NF & (f " {+infty }) /\ (g " {-infty }) c= NG ) by XBOOLE_1:1;
then A8: ((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty })) c= NF \/ NG by XBOOLE_1:13;
then A9: E0 \ (NF \/ NG) c= dom (f + g) by A1, A2, A7, XBOOLE_1:34;
then A10: ( (f + g) | (E0 \ (NF \/ NG)) = (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) & dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) ) by Th35;
reconsider DFPG = dom (f + g) as Element of S by A1, Th113;
set NFPG = DFPG \ (E0 \ (NF \/ NG));
DFPG \ (E0 \ (NF \/ NG)) c= E0 \ (E0 \ (NF \/ NG)) by A1, A2, A7, XBOOLE_1:33, XBOOLE_1:36;
then A11: DFPG \ (E0 \ (NF \/ NG)) c= E0 /\ (NF \/ NG) by XBOOLE_1:48;
E0 /\ (NF \/ NG) c= NF \/ NG by XBOOLE_1:17;
then DFPG \ (E0 \ (NF \/ NG)) is measure_zero of M by A4, A11, MEASURE1:69, XBOOLE_1:1;
then A12: M . (DFPG \ (E0 \ (NF \/ NG))) = 0 by MEASURE1:def 13;
DFPG \ (DFPG \ (E0 \ (NF \/ NG))) = DFPG /\ (E0 \ (NF \/ NG)) by XBOOLE_1:48;
then A13: E0 \ (NF \/ NG) = DFPG \ (DFPG \ (E0 \ (NF \/ NG))) by A1, A2, A7, A8, XBOOLE_1:28, XBOOLE_1:34;
A14: DFPG \ (E0 \ (NF \/ NG)) c= dom (f + g) by XBOOLE_1:36;
A15: ( E0 \ (NF \/ NG) c= dom f & E0 \ (NF \/ NG) c= dom g ) by A1, A2, XBOOLE_1:36;
A16: ( f is_measurable_on E0 \ (NF \/ NG) & g is_measurable_on E0 \ (NF \/ NG) ) by A1, A2, A3, MESFUNC1:34, XBOOLE_1:36;
A17: ( dom (f | (E0 \ (NF \/ NG))) = (dom f) /\ (E0 \ (NF \/ NG)) & dom (g | (E0 \ (NF \/ NG))) = (dom g) /\ (E0 \ (NF \/ NG)) ) by RELAT_1:90;
then A18: ( E0 \ (NF \/ NG) = dom (f | (E0 \ (NF \/ NG))) & E0 \ (NF \/ NG) = dom (g | (E0 \ (NF \/ NG))) ) by A1, A2, XBOOLE_1:28, XBOOLE_1:36;
then A19: ( f | (E0 \ (NF \/ NG)) is_measurable_on E0 \ (NF \/ NG) & g | (E0 \ (NF \/ NG)) is_measurable_on E0 \ (NF \/ NG) ) by A16, A17, Th48;
A20: 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 ) )
assume A21: x in dom (f | (E0 \ (NF \/ NG))) ; :: thesis: ( (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;
x in (dom f) /\ (E0 \ (NF \/ NG)) by A21, RELAT_1:90;
then A22: ( x in dom f & x in E0 \ (NF \/ NG) ) by XBOOLE_0:def 4;
then A23: not x in NF \/ NG by XBOOLE_0:def 5;

A24: now

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

end;

now

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

end;

hence ( (f | (E0 \ (NF \/ NG))) . x < +infty & -infty < (f | (E0 \ (NF \/ NG))) . x ) by A24, 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 ) & ( for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds
(f | (E0 \ (NF \/ NG))) . x < +infty ) ) ;
then A27: ( f | (E0 \ (NF \/ NG)) is without-infty & f | (E0 \ (NF \/ NG)) is without+infty ) by Th16, Th17;
A28: 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 ) )
assume A29: x in dom (g | (E0 \ (NF \/ NG))) ; :: thesis: ( -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;
x in (dom g) /\ (E0 \ (NF \/ NG)) by A29, RELAT_1:90;
then A30: ( x in dom g & x in E0 \ (NF \/ NG) ) by XBOOLE_0:def 4;
then A31: not x in NF \/ NG by XBOOLE_0:def 5;

A32: now

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

end;

now

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

end;

hence ( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty ) by A32, 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 ) & ( for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds
(g | (E0 \ (NF \/ NG))) . x < +infty ) ) ;
then A35: ( g | (E0 \ (NF \/ NG)) is without-infty & g | (E0 \ (NF \/ NG)) is without+infty ) by Th16, Th17;

now

let x be Element of X; :: thesis: ( x in dom (f | (E0 \ (NF \/ NG))) implies |.((f | (E0 \ (NF \/ NG))) . x).| < +infty )
assume x in dom (f | (E0 \ (NF \/ NG))) ; :: thesis: |.((f | (E0 \ (NF \/ NG))) . x).| < +infty
then A36: ( -infty < (f | (E0 \ (NF \/ NG))) . x & (f | (E0 \ (NF \/ NG))) . x < +infty ) by A20;
- +infty = -infty by XXREAL_3:def 3;
hence |.((f | (E0 \ (NF \/ NG))) . x).| < +infty by A36, EXTREAL2:59; :: thesis: verum

end;

then A37: f | (E0 \ (NF \/ NG)) is real-valued by MESFUNC2:def 1;

now

let x be Element of X; :: thesis: ( x in dom (g | (E0 \ (NF \/ NG))) implies |.((g | (E0 \ (NF \/ NG))) . x).| < +infty )
assume x in dom (g | (E0 \ (NF \/ NG))) ; :: thesis: |.((g | (E0 \ (NF \/ NG))) . x).| < +infty
then A38: ( -infty < (g | (E0 \ (NF \/ NG))) . x & (g | (E0 \ (NF \/ NG))) . x < +infty ) by A28;
- +infty = -infty by XXREAL_3:def 3;
hence |.((g | (E0 \ (NF \/ NG))) . x).| < +infty by A38, EXTREAL2:59; :: thesis: verum

end;

then A39: g | (E0 \ (NF \/ NG)) is real-valued by MESFUNC2:def 1;
then A40: ( E0 \ (NF \/ NG) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) & (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) ) by A9, A19, A37, Th35, MESFUNC2:7;
A41: ( f | (E0 \ (NF \/ NG)) is_integrable_on M & g | (E0 \ (NF \/ NG)) is_integrable_on M ) by A1, Th103;
then A42: (f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))) is_integrable_on M by Th114;
( ( for x being set st x in dom (f | (E0 \ (NF \/ NG))) holds
-infty < (f | (E0 \ (NF \/ NG))) . x ) & ( for x being set st x in dom (g | (E0 \ (NF \/ NG))) holds
-infty < (g | (E0 \ (NF \/ NG))) . x ) ) by A20, A28;
then A43: ( f | (E0 \ (NF \/ NG)) is without-infty & g | (E0 \ (NF \/ NG)) is without-infty ) by Th16;
then ( 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)))) & 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 Th30;
then A44: ( dom ((max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG))))) = E0 \ (NF \/ NG) & dom (max- (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) & dom ((max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG))))) = E0 \ (NF \/ NG) & dom (max+ (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) ) by A18, MESFUNC2:def 2, MESFUNC2:def 3;
A45: ( (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is nonnegative & (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG)))) is nonnegative ) by A43, Th30;
A46: ( dom (max- (f | (E0 \ (NF \/ NG)))) = dom (f | (E0 \ (NF \/ NG))) & dom (max+ (f | (E0 \ (NF \/ NG)))) = dom (f | (E0 \ (NF \/ NG))) & dom (max- (g | (E0 \ (NF \/ NG)))) = dom (g | (E0 \ (NF \/ NG))) & dom (max+ (g | (E0 \ (NF \/ NG)))) = dom (g | (E0 \ (NF \/ NG))) & dom (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) & dom (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) = dom ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) ) by MESFUNC2:def 2, MESFUNC2:def 3;
A47: ( max+ (f | (E0 \ (NF \/ NG))) is nonnegative & max- (f | (E0 \ (NF \/ NG))) is nonnegative & max- (g | (E0 \ (NF \/ NG))) is nonnegative & max+ (g | (E0 \ (NF \/ NG))) is nonnegative & max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is nonnegative & max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is nonnegative ) by Lm1;
A48: ( max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is_measurable_on E0 \ (NF \/ NG) & max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))) is_measurable_on E0 \ (NF \/ NG) ) by A40, MESFUNC2:27, MESFUNC2:28;
A49: max- (f | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) by A18, A19, MESFUNC2:28;
A50: ((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 A27, A35, Th31;
A51: ( max+ (g | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) & max+ (f | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) ) by A19, MESFUNC2:27;
(dom (f | (E0 \ (NF \/ NG)))) /\ (dom (g | (E0 \ (NF \/ NG)))) = E0 \ (NF \/ NG) by A1, A2, A17, XBOOLE_1:28, XBOOLE_1:36;
then (max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max+ (f | (E0 \ (NF \/ NG)))) is_measurable_on E0 \ (NF \/ NG) by A19, A43, Th50;
then A52: 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 A44, A45, A47, A51, Lm11
.= ((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 A10, A18, A46, A47, A48, A51, Lm11 ;
A53: ( 0 <= integral+ M,(max+ (f | (E0 \ (NF \/ NG)))) & integral+ M,(max+ (f | (E0 \ (NF \/ NG)))) <> +infty & 0 <= integral+ M,(max- (f | (E0 \ (NF \/ NG)))) & integral+ M,(max- (f | (E0 \ (NF \/ NG)))) <> +infty & 0 <= integral+ M,(max+ (g | (E0 \ (NF \/ NG)))) & integral+ M,(max+ (g | (E0 \ (NF \/ NG)))) <> +infty & 0 <= integral+ M,(max- (g | (E0 \ (NF \/ NG)))) & integral+ M,(max- (g | (E0 \ (NF \/ NG)))) <> +infty & 0 <= integral+ M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) & integral+ M,(max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) <> +infty & 0 <= integral+ M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) & integral+ M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) <> +infty ) by A41, A42, Def17, Th102;
then A54: ( - (integral+ M,(max- (f | (E0 \ (NF \/ NG))))) <> -infty & - (integral+ M,(max- (f | (E0 \ (NF \/ NG))))) <> +infty & - (integral+ M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) <> +infty & - (integral+ M,(max- ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG)))))) <> -infty ) by XXREAL_3:23;
( (max+ ((f | (E0 \ (NF \/ NG))) + (g | (E0 \ (NF \/ NG))))) + (max- (f | (E0 \ (NF \/ NG)))) is_measurable_on E0 \ (NF \/ NG) & max- (g | (E0 \ (NF \/ NG))) is_measurable_on E0 \ (NF \/ NG) ) by A18, A19, A43, Th49, MESFUNC2:28;
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 A44, A45, A47, Lm11
.= ((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 A10, A18, A46, A47, A48, A49, Lm11 ;
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 A50, A52, A53, 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 A53, 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 (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;
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 A53, 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 A53, 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 A53, A54, 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 A53, A54, 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 A53, A54, 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 A55: 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;
A56: Integral M,f = Integral M,(f | (E0 \ (NF \/ NG))) by A2, A5, Th101;
Integral M,g = Integral M,(g | (E0 \ (NF \/ NG))) by A1, A2, A3, A5, 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 real-valued & 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 real-valued & 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 A1, A2, A5, A6, A9, A10, A12, A13, A14, A15, A18, A19, A37, A39, A40, A41, A55, A56, Th114; :: thesis: verum