let A be non empty closed_interval Subset of REAL; :: thesis:
let f, g be Function of A,REAL; :: thesis:
assume that
A1: f | A is bounded and
A2: g | A is bounded and
A3: f is integrable and
A4: g is integrable ; :: thesis:
A5: (lower_integral f) + (lower_integral g) = (upper_integral f) + (lower_integral g) by A3
.= (integral f) + (integral g) by A4 ;
A6: (f + g) | (A /\ A) is bounded by A1, A2, RFUNCT_1:83;
for D being object st D in (divs A) /\ (dom (lower_sum_set (f + g))) holds
(lower_sum_set (f + g)) . D <= ((upper_bound (rng f)) * (vol A)) + ((upper_bound (rng g)) * (vol A))

proof

let D be object ; :: thesis:
assume D in (divs A) /\ (dom (lower_sum_set (f + g))) ; :: thesis:
then reconsider D = D as Division of A by Def2;
(lower_sum_set (f + g)) . D = lower_sum ((f + g),D) by Def10;
then A7: (lower_sum_set (f + g)) . D <= upper_sum ((f + g),D) by A6, Th26;
upper_sum (f,D) <= (upper_bound (rng f)) * (vol A) by A1, Th25;
then A8: (upper_sum (f,D)) + (upper_sum (g,D)) <= ((upper_bound (rng f)) * (vol A)) + (upper_sum (g,D)) by XREAL_1:6;
upper_sum (g,D) <= (upper_bound (rng g)) * (vol A) by A2, Th25;
then A9: ((upper_bound (rng f)) * (vol A)) + (upper_sum (g,D)) <= ((upper_bound (rng f)) * (vol A)) + ((upper_bound (rng g)) * (vol A)) by XREAL_1:6;
upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D)) by A1, A2, Th53;
then (lower_sum_set (f + g)) . D <= (upper_sum (f,D)) + (upper_sum (g,D)) by A7, XXREAL_0:2;
then (lower_sum_set (f + g)) . D <= ((upper_bound (rng f)) * (vol A)) + (upper_sum (g,D)) by A8, XXREAL_0:2;
hence (lower_sum_set (f + g)) . D <= ((upper_bound (rng f)) * (vol A)) + ((upper_bound (rng g)) * (vol A)) by A9, XXREAL_0:2; :: thesis:

end;

then (lower_sum_set (f + g)) | (divs A) is bounded_above by RFUNCT_1:70;
then A10: rng (lower_sum_set (f + g)) is bounded_above by Th11;
then A11: f + g is lower_integrable ;
for D being object st D in (divs A) /\ (dom (upper_sum_set (f + g))) holds
((lower_bound (rng f)) * (vol A)) + ((lower_bound (rng g)) * (vol A)) <= (upper_sum_set (f + g)) . D

proof

let D be object ; :: thesis:
assume D in (divs A) /\ (dom (upper_sum_set (f + g))) ; :: thesis:
then reconsider D = D as Division of A by Def2;
(upper_sum_set (f + g)) . D = upper_sum ((f + g),D) by Def9;
then A12: lower_sum ((f + g),D) <= (upper_sum_set (f + g)) . D by A6, Th26;
(lower_bound (rng f)) * (vol A) <= lower_sum (f,D) by A1, Th23;
then A13: ((lower_bound (rng f)) * (vol A)) + (lower_sum (g,D)) <= (lower_sum (f,D)) + (lower_sum (g,D)) by XREAL_1:6;
(lower_bound (rng g)) * (vol A) <= lower_sum (g,D) by A2, Th23;
then A14: ((lower_bound (rng f)) * (vol A)) + ((lower_bound (rng g)) * (vol A)) <= ((lower_bound (rng f)) * (vol A)) + (lower_sum (g,D)) by XREAL_1:6;
(lower_sum (f,D)) + (lower_sum (g,D)) <= lower_sum ((f + g),D) by A1, A2, Th54;
then (lower_sum (f,D)) + (lower_sum (g,D)) <= (upper_sum_set (f + g)) . D by A12, XXREAL_0:2;
then ((lower_bound (rng f)) * (vol A)) + (lower_sum (g,D)) <= (upper_sum_set (f + g)) . D by A13, XXREAL_0:2;
hence ((lower_bound (rng f)) * (vol A)) + ((lower_bound (rng g)) * (vol A)) <= (upper_sum_set (f + g)) . D by A14, XXREAL_0:2; :: thesis:

end;

then (upper_sum_set (f + g)) | (divs A) is bounded_below by RFUNCT_1:71;
then A15: rng (upper_sum_set (f + g)) is bounded_below by Th9;
A16: for D being Division of A st D in (divs A) /\ (dom (upper_sum_set (f + g))) holds
((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_integral (f + g)

proof

let D be Division of A; :: thesis:
(upper_sum (f,D)) + (upper_sum (g,D)) >= upper_sum ((f + g),D) by A1, A2, Th53;
then A17: ((upper_sum_set f) . D) + (upper_sum (g,D)) >= upper_sum ((f + g),D) by Def9;
assume D in (divs A) /\ (dom (upper_sum_set (f + g))) ; :: thesis:
then D in dom (upper_sum_set (f + g)) by XBOOLE_0:def 4;
then (upper_sum_set (f + g)) . D in rng (upper_sum_set (f + g)) by FUNCT_1:def 3;
then A18: (upper_sum_set (f + g)) . D >= upper_integral (f + g) by A15, SEQ_4:def 2;
((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_sum ((f + g),D) by A17, Def9;
then ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= (upper_sum_set (f + g)) . D by Def9;
hence ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_integral (f + g) by A18, XXREAL_0:2; :: thesis:

end;

A19: dom (upper_sum_set (f + g)) = divs A by FUNCT_2:def 1;
A20: for a1 being Real st a1 in rng (upper_sum_set f) holds
a1 >= (upper_integral (f + g)) - (upper_integral g)

proof

let a1 be Real; :: thesis:
assume a1 in rng (upper_sum_set f) ; :: thesis:
then consider D1 being Element of divs A such that
D1 in dom (upper_sum_set f) and
A21: a1 = (upper_sum_set f) . D1 by PARTFUN1:3;
reconsider D1 = D1 as Division of A by Def2;
A22: a1 = upper_sum (f,D1) by A21, Def9;
for a2 being Real st a2 in rng (upper_sum_set g) holds
a2 >= (upper_integral (f + g)) - a1

proof

let a2 be Real; :: thesis:
assume a2 in rng (upper_sum_set g) ; :: thesis:
then consider D2 being Element of divs A such that
D2 in dom (upper_sum_set g) and
A23: a2 = (upper_sum_set g) . D2 by PARTFUN1:3;
reconsider D2 = D2 as Division of A by Def2;
consider D being Division of A such that
A24: D1 <= D and
A25: D2 <= D by Th45;
A26: D in divs A by Def2;
(upper_sum_set g) . D = upper_sum (g,D) by Def9;
then A27: (upper_sum_set g) . D <= upper_sum (g,D2) by A2, A25, Th43;
(upper_sum_set f) . D = upper_sum (f,D) by Def9;
then (upper_sum_set f) . D <= upper_sum (f,D1) by A1, A24, Th43;
then A28: ((upper_sum_set f) . D) + ((upper_sum_set g) . D) <= (upper_sum (f,D1)) + (upper_sum (g,D2)) by A27, XREAL_1:7;
((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_integral (f + g) by A19, A16, A26;
then A29: (upper_sum (f,D1)) + (upper_sum (g,D2)) >= upper_integral (f + g) by A28, XXREAL_0:2;
a2 = upper_sum (g,D2) by A23, Def9;
hence a2 >= (upper_integral (f + g)) - a1 by A22, A29, XREAL_1:20; :: thesis:

end;

then lower_bound (rng (upper_sum_set g)) >= (upper_integral (f + g)) - a1 by SEQ_4:43;
then a1 + (lower_bound (rng (upper_sum_set g))) >= upper_integral (f + g) by XREAL_1:20;
hence a1 >= (upper_integral (f + g)) - (upper_integral g) by XREAL_1:20; :: thesis:

end;

upper_integral f >= (upper_integral (f + g)) - (upper_integral g) by A20, SEQ_4:43;
then A30: (integral f) + (upper_integral g) >= upper_integral (f + g) by XREAL_1:20;
A31: for D being Division of A st D in (divs A) /\ (dom (lower_sum_set (f + g))) holds
((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_integral (f + g)

proof

let D be Division of A; :: thesis:
(lower_sum (f,D)) + (lower_sum (g,D)) <= lower_sum ((f + g),D) by A1, A2, Th54;
then A32: ((lower_sum_set f) . D) + (lower_sum (g,D)) <= lower_sum ((f + g),D) by Def10;
assume D in (divs A) /\ (dom (lower_sum_set (f + g))) ; :: thesis:
then D in dom (lower_sum_set (f + g)) by XBOOLE_0:def 4;
then (lower_sum_set (f + g)) . D in rng (lower_sum_set (f + g)) by FUNCT_1:def 3;
then A33: (lower_sum_set (f + g)) . D <= lower_integral (f + g) by A10, SEQ_4:def 1;
((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_sum ((f + g),D) by A32, Def10;
then ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= (lower_sum_set (f + g)) . D by Def10;
hence ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_integral (f + g) by A33, XXREAL_0:2; :: thesis:

end;

A34: dom (lower_sum_set (f + g)) = divs A by FUNCT_2:def 1;
A35: for a1 being Real st a1 in rng (lower_sum_set f) holds
a1 <= (lower_integral (f + g)) - (lower_integral g)

proof

let a1 be Real; :: thesis:
assume a1 in rng (lower_sum_set f) ; :: thesis:
then consider D1 being Element of divs A such that
D1 in dom (lower_sum_set f) and
A36: a1 = (lower_sum_set f) . D1 by PARTFUN1:3;
reconsider D1 = D1 as Division of A by Def2;
A37: a1 = lower_sum (f,D1) by A36, Def10;
for a2 being Real st a2 in rng (lower_sum_set g) holds
a2 <= (lower_integral (f + g)) - a1

proof

let a2 be Real; :: thesis:
assume a2 in rng (lower_sum_set g) ; :: thesis:
then consider D2 being Element of divs A such that
D2 in dom (lower_sum_set g) and
A38: a2 = (lower_sum_set g) . D2 by PARTFUN1:3;
reconsider D2 = D2 as Division of A by Def2;
consider D being Division of A such that
A39: D1 <= D and
A40: D2 <= D by Th45;
A41: D in divs A by Def2;
(lower_sum_set g) . D = lower_sum (g,D) by Def10;
then A42: (lower_sum_set g) . D >= lower_sum (g,D2) by A2, A40, Th44;
(lower_sum_set f) . D = lower_sum (f,D) by Def10;
then (lower_sum_set f) . D >= lower_sum (f,D1) by A1, A39, Th44;
then A43: ((lower_sum_set f) . D) + ((lower_sum_set g) . D) >= (lower_sum (f,D1)) + (lower_sum (g,D2)) by A42, XREAL_1:7;
((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_integral (f + g) by A34, A31, A41;
then A44: (lower_sum (f,D1)) + (lower_sum (g,D2)) <= lower_integral (f + g) by A43, XXREAL_0:2;
a2 = lower_sum (g,D2) by A38, Def10;
hence a2 <= (lower_integral (f + g)) - a1 by A37, A44, XREAL_1:19; :: thesis:

end;

then upper_bound (rng (lower_sum_set g)) <= (lower_integral (f + g)) - a1 by SEQ_4:45;
then a1 + (upper_bound (rng (lower_sum_set g))) <= lower_integral (f + g) by XREAL_1:19;
hence a1 <= (lower_integral (f + g)) - (lower_integral g) by XREAL_1:19; :: thesis:

end;

upper_bound (rng (lower_sum_set f)) <= (lower_integral (f + g)) - (lower_integral g) by A35, SEQ_4:45;
then A45: (lower_integral f) + (lower_integral g) <= lower_integral (f + g) by XREAL_1:19;
A46: upper_integral (f + g) >= lower_integral (f + g) by A6, Th47;
then (integral f) + (integral g) <= upper_integral (f + g) by A45, A5, XXREAL_0:2;
then upper_integral (f + g) = (integral f) + (integral g) by A30, XXREAL_0:1;
then A47: upper_integral (f + g) = lower_integral (f + g) by A45, A46, A5, XXREAL_0:1;
f + g is upper_integrable by A15;
hence ( f + g is integrable & integral (f + g) = (integral f) + (integral g) ) by A11, A45, A5, A30, A47, XXREAL_0:1; :: thesis: