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;
now :: thesis: for x being object st x in dom g holds
(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;
then A8: g = max+ g by A6, FUNCT_1: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;
now :: thesis: for x being object st x in dom f holds
(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;
then A22: f = max+ f by A20, FUNCT_1:2;
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
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;
then A29: f + g = max+ (f + g) by A23, FUNCT_1:2;
A30: now :: thesis: for x being Element of X st x in dom (max- (f + g)) holds
(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;
integral+ (M,(f | C)) <= integral+ (M,(f | A)) by A3, A11, A12, A17, A15, Th83, XBOOLE_1:17;
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