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 that

A1: f is_integrable_on M and

A2: g is_integrable_on M and

A3: f is nonnegative and

A4: g is nonnegative ; :: thesis: f + g is_integrable_on M

A5: integral+ (M,(max+ g)) < +infty by A2;

A6: dom g = dom (max+ g) by MESFUNC2:def 2;

consider B being Element of S such that

A9: B = dom g and

A10: g is B -measurable by A2;

consider A being Element of S such that

A11: A = dom f and

A12: f is A -measurable by A1;

A13: g is A /\ B -measurable by A10, MESFUNC1:30, XBOOLE_1:17;

f is A /\ B -measurable by A12, MESFUNC1:30, XBOOLE_1:17;

then A14: f + g is A /\ B -measurable by A3, A4, A13, Th31;

consider C being Element of S such that

A15: C = dom (f + g) and

A16: integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) by A3, A4, A11, A12, A9, A10, Th78;

A17: A /\ B = dom (f + g) by A3, A4, A11, A9, Th16;

then integral+ (M,(g | C)) <= integral+ (M,(g | B)) by A4, A9, A10, A15, Th83, XBOOLE_1:17;

then A18: integral+ (M,(g | C)) <= integral+ (M,(max+ g)) by A9, A8, GRFUNC_1:23;

integral+ (M,(max+ f)) < +infty by A1;

then A19: (integral+ (M,(max+ f))) + (integral+ (M,(max+ g))) < +infty by A5, XXREAL_0:4, XXREAL_3:16;

A20: dom f = dom (max+ f) by MESFUNC2:def 2;

A23: dom (f + g) = dom (max+ (f + g)) by MESFUNC2:def 2;

then integral+ (M,(f | C)) <= integral+ (M,(max+ f)) by A11, A22, GRFUNC_1:23;

then integral+ (M,(max+ (f + g))) <= (integral+ (M,(max+ f))) + (integral+ (M,(max+ g))) by A29, A16, A18, XXREAL_3:36;

then A31: integral+ (M,(max+ (f + g))) < +infty by A19, XXREAL_0:4;

dom (f + g) = dom (max- (f + g)) by MESFUNC2:def 3;

then integral+ (M,(max- (f + g))) = 0 by A17, A14, A30, Th87, MESFUNC2:26;

hence f + g is_integrable_on M by A17, A14, A31; :: 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 & 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 that

A1: f is_integrable_on M and

A2: g is_integrable_on M and

A3: f is nonnegative and

A4: g is nonnegative ; :: thesis: f + g is_integrable_on M

A5: integral+ (M,(max+ g)) < +infty by A2;

A6: dom g = dom (max+ g) by MESFUNC2:def 2;

now :: thesis: for x being object st x in dom g holds

(max+ g) . x = g . x

then A8:
g = max+ g
by A6, FUNCT_1:2;(max+ g) . x = g . x

let x be object ; :: thesis: ( x in dom g implies (max+ g) . x = g . x )

assume x in dom g ; :: thesis: (max+ g) . x = g . x

then A7: (max+ g) . x = max ((g . x),0) by A6, MESFUNC2:def 2;

0 <= g . x by A4, SUPINF_2:51;

hence (max+ g) . x = g . x by A7, XXREAL_0:def 10; :: thesis: verum

end;assume x in dom g ; :: thesis: (max+ g) . x = g . x

then A7: (max+ g) . x = max ((g . x),0) by A6, MESFUNC2:def 2;

0 <= g . x by A4, SUPINF_2:51;

hence (max+ g) . x = g . x by A7, XXREAL_0:def 10; :: thesis: verum

consider B being Element of S such that

A9: B = dom g and

A10: g is B -measurable by A2;

consider A being Element of S such that

A11: A = dom f and

A12: f is A -measurable by A1;

A13: g is A /\ B -measurable by A10, MESFUNC1:30, XBOOLE_1:17;

f is A /\ B -measurable by A12, MESFUNC1:30, XBOOLE_1:17;

then A14: f + g is A /\ B -measurable by A3, A4, A13, Th31;

consider C being Element of S such that

A15: C = dom (f + g) and

A16: integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) by A3, A4, A11, A12, A9, A10, Th78;

A17: A /\ B = dom (f + g) by A3, A4, A11, A9, Th16;

then integral+ (M,(g | C)) <= integral+ (M,(g | B)) by A4, A9, A10, A15, Th83, XBOOLE_1:17;

then A18: integral+ (M,(g | C)) <= integral+ (M,(max+ g)) by A9, A8, GRFUNC_1:23;

integral+ (M,(max+ f)) < +infty by A1;

then A19: (integral+ (M,(max+ f))) + (integral+ (M,(max+ g))) < +infty by A5, XXREAL_0:4, XXREAL_3:16;

A20: dom f = dom (max+ f) by MESFUNC2:def 2;

now :: thesis: for x being object st x in dom f holds

(max+ f) . x = f . x

then A22:
f = max+ f
by A20, FUNCT_1:2;(max+ f) . x = f . x

let x be object ; :: thesis: ( x in dom f implies (max+ f) . x = f . x )

assume x in dom f ; :: thesis: (max+ f) . x = f . x

then A21: (max+ f) . x = max ((f . x),0) by A20, MESFUNC2:def 2;

0 <= f . x by A3, SUPINF_2:51;

hence (max+ f) . x = f . x by A21, XXREAL_0:def 10; :: thesis: verum

end;assume x in dom f ; :: thesis: (max+ f) . x = f . x

then A21: (max+ f) . x = max ((f . x),0) by A20, MESFUNC2:def 2;

0 <= f . x by A3, SUPINF_2:51;

hence (max+ f) . x = f . x by A21, XXREAL_0:def 10; :: thesis: verum

A23: dom (f + g) = dom (max+ (f + g)) by MESFUNC2:def 2;

A24: now :: thesis: for x being object st x in dom (f + g) holds

(max+ (f + g)) . x = (f + g) . x

then A29:
f + g = max+ (f + g)
by A23, FUNCT_1:2;(max+ (f + g)) . x = (f + g) . x

let x be object ; :: thesis: ( x in dom (f + g) implies (max+ (f + g)) . x = (f + g) . x )

assume A25: x in dom (f + g) ; :: thesis: (max+ (f + g)) . x = (f + g) . x

then A26: (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3;

A27: 0 <= g . x by A4, SUPINF_2:51;

A28: 0 <= f . x by A3, SUPINF_2:51;

(max+ (f + g)) . x = max (((f + g) . x),0) by A23, A25, MESFUNC2:def 2;

hence (max+ (f + g)) . x = (f + g) . x by A26, A28, A27, XXREAL_0:def 10; :: thesis: verum

end;assume A25: x in dom (f + g) ; :: thesis: (max+ (f + g)) . x = (f + g) . x

then A26: (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3;

A27: 0 <= g . x by A4, SUPINF_2:51;

A28: 0 <= f . x by A3, SUPINF_2:51;

(max+ (f + g)) . x = max (((f + g) . x),0) by A23, A25, MESFUNC2:def 2;

hence (max+ (f + g)) . x = (f + g) . x by A26, A28, A27, XXREAL_0:def 10; :: thesis: verum

A30: now :: thesis: for x being Element of X st x in dom (max- (f + g)) holds

(max- (f + g)) . x = 0

integral+ (M,(f | C)) <= integral+ (M,(f | A))
by A3, A11, A12, A17, A15, Th83, XBOOLE_1:17;(max- (f + g)) . x = 0

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 A24;

hence (max- (f + g)) . x = 0 by MESFUNC2:19; :: thesis: verum

end;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 A24;

hence (max- (f + g)) . x = 0 by MESFUNC2:19; :: thesis: verum

then integral+ (M,(f | C)) <= integral+ (M,(max+ f)) by A11, A22, GRFUNC_1:23;

then integral+ (M,(max+ (f + g))) <= (integral+ (M,(max+ f))) + (integral+ (M,(max+ g))) by A29, A16, A18, XXREAL_3:36;

then A31: integral+ (M,(max+ (f + g))) < +infty by A19, XXREAL_0:4;

dom (f + g) = dom (max- (f + g)) by MESFUNC2:def 3;

then integral+ (M,(max- (f + g))) = 0 by A17, A14, A30, Th87, MESFUNC2:26;

hence f + g is_integrable_on M by A17, A14, A31; :: thesis: verum