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 & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
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 & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
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 & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative implies f + g is_integrable_on M )
assume A1: ( f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative ) ; :: thesis: f + g is_integrable_on M
then consider A being Element of S such that
A2: ( A = dom f & f is_measurable_on A ) by Def17;
consider B being Element of S such that
A3: ( B = dom g & g is_measurable_on B ) by A1, Def17;
( f is_measurable_on A /\ B & g is_measurable_on A /\ B ) by A2, A3, MESFUNC1:34, XBOOLE_1:17;
then A4: ( A /\ B = dom (f + g) & f + g is_measurable_on A /\ B ) by A1, A2, A3, Th22, Th37;
A5: ( dom (f + g) = dom (max+ (f + g)) & dom f = dom (max+ f) & dom g = dom (max+ g) ) by MESFUNC2:def 2;

A6: now

let x be set ; :: thesis: ( x in dom (f + g) implies (max+ (f + g)) . x = (f + g) . x )
assume A7: x in dom (f + g) ; :: thesis: (max+ (f + g)) . x = (f + g) . x
then A8: (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3;
B9: ( 0 <= f . x & 0 <= g . x ) by A1, SUPINF_2:70;
(max+ (f + g)) . x = max ((f + g) . x),0 by A5, A7, MESFUNC2:def 2;
hence (max+ (f + g)) . x = (f + g) . x by B9, A8, XXREAL_0:def 10; :: thesis: verum

end;

then A10: f + g = max+ (f + g) by A5, FUNCT_1:9;

now

let x be set ; :: thesis: ( x in dom g implies (max+ g) . x = g . x )
assume A11: x in dom g ; :: thesis: (max+ g) . x = g . x
A12: 0 <= g . x by A1, SUPINF_2:70;
(max+ g) . x = max (g . x),0 by A5, A11, MESFUNC2:def 2;
hence (max+ g) . x = g . x by A12, XXREAL_0:def 10; :: thesis: verum

end;

then A13: g = max+ g by A5, FUNCT_1:9;

now

let x be set ; :: thesis: ( x in dom f implies (max+ f) . x = f . x )
assume A14: x in dom f ; :: thesis: (max+ f) . x = f . x
A15: 0 <= f . x by A1, SUPINF_2:70;
(max+ f) . x = max (f . x),0 by A5, A14, MESFUNC2:def 2;
hence (max+ f) . x = f . x by A15, XXREAL_0:def 10; :: thesis: verum

end;

then A16: f = max+ f by A5, FUNCT_1:9;

A17: now

let x be Element of X; :: thesis: ( x in dom (max- (f + g)) implies (max- (f + g)) . x = 0 )
assume x in dom (max- (f + g)) ; :: thesis: (max- (f + g)) . x = 0
then x in dom (f + g) by MESFUNC2:def 3;
then (max+ (f + g)) . x = (f + g) . x by A6;
hence (max- (f + g)) . x = 0 by MESFUNC2:21; :: thesis: verum

end;

A18: dom (f + g) = dom (max- (f + g)) by MESFUNC2:def 3;
A19: integral+ M,(max- (f + g)) = 0 by A4, A17, A18, Th93, MESFUNC2:28;
consider C being Element of S such that
A20: ( C = dom (f + g) & integral+ M,(f + g) = (integral+ M,(f | C)) + (integral+ M,(g | C)) ) by A1, A2, A3, Th84;
( integral+ M,(f | C) <= integral+ M,(f | A) & integral+ M,(g | C) <= integral+ M,(g | B) ) by A1, A2, A3, A4, A20, Th89, XBOOLE_1:17;
then A21: ( integral+ M,(f | C) <= integral+ M,(max+ f) & integral+ M,(g | C) <= integral+ M,(max+ g) ) by A2, A3, A13, A16, GRFUNC_1:64;
( integral+ M,(max+ f) < +infty & integral+ M,(max+ g) < +infty ) by A1, Def17;
then A23: (integral+ M,(max+ f)) + (integral+ M,(max+ g)) < +infty by XXREAL_0:4, XXREAL_3:16;
integral+ M,(max+ (f + g)) <= (integral+ M,(max+ f)) + (integral+ M,(max+ g)) by A10, A20, A21, XXREAL_3:38;
then integral+ M,(max+ (f + g)) < +infty by A23, XXREAL_0:4;
hence f + g is_integrable_on M by A4, A19, Def17; :: thesis: verum