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, Def17
.= (integral f) + (integral g) by A4, Def17 ;
A6: (f + g) | (A /\ A) is bounded by A1, A2, RFUNCT_1:83;
for D being set 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 set ; :: thesis:
assume A7: D in (divs A) /\ (dom (lower_sum_set (f + g))) ; :: thesis:
then reconsider D = D as Division of A by Def3;
(lower_sum_set (f + g)) . D = lower_sum ((f + g),D) by Def12;
then A8: (lower_sum_set (f + g)) . D <= upper_sum ((f + g),D) by A6, Th30;
upper_sum (f,D) <= (upper_bound (rng f)) * (vol A) by A1, Th29;
then A9: (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, Th29;
then A10: ((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, Th57;
then (lower_sum_set (f + g)) . D <= (upper_sum (f,D)) + (upper_sum (g,D)) by A8, XXREAL_0:2;
then (lower_sum_set (f + g)) . D <= ((upper_bound (rng f)) * (vol A)) + (upper_sum (g,D)) by A9, XXREAL_0:2;
hence (lower_sum_set (f + g)) . D <= ((upper_bound (rng f)) * (vol A)) + ((upper_bound (rng g)) * (vol A)) by A10, XXREAL_0:2; :: thesis:

end;

then (lower_sum_set (f + g)) | (divs A) is bounded_above by RFUNCT_1:70;
then A11: rng (lower_sum_set (f + g)) is bounded_above by Th15;
then A12: f + g is lower_integrable by Def14;
for D being set 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 set ; :: thesis:
assume A13: D in (divs A) /\ (dom (upper_sum_set (f + g))) ; :: thesis:
then reconsider D = D as Division of A by Def3;
(upper_sum_set (f + g)) . D = upper_sum ((f + g),D) by Def11;
then A14: lower_sum ((f + g),D) <= (upper_sum_set (f + g)) . D by A6, Th30;
(lower_bound (rng f)) * (vol A) <= lower_sum (f,D) by A1, Th27;
then A15: ((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, Th27;
then A16: ((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, Th58;
then (lower_sum (f,D)) + (lower_sum (g,D)) <= (upper_sum_set (f + g)) . D by A14, XXREAL_0:2;
then ((lower_bound (rng f)) * (vol A)) + (lower_sum (g,D)) <= (upper_sum_set (f + g)) . D by A15, XXREAL_0:2;
hence ((lower_bound (rng f)) * (vol A)) + ((lower_bound (rng g)) * (vol A)) <= (upper_sum_set (f + g)) . D by A16, XXREAL_0:2; :: thesis:

end;

then (upper_sum_set (f + g)) | (divs A) is bounded_below by RFUNCT_1:71;
then A17: rng (upper_sum_set (f + g)) is bounded_below by Th13;
A18: 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:
A19: D in divs A by Def3;
(upper_sum (f,D)) + (upper_sum (g,D)) >= upper_sum ((f + g),D) by A1, A2, Th57;
then A21: ((upper_sum_set f) . D) + (upper_sum (g,D)) >= upper_sum ((f + g),D) by Def11;
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 A23: (upper_sum_set (f + g)) . D >= upper_integral (f + g) by A17, SEQ_4:def 2;
((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_sum ((f + g),D) by A21, Def11;
then ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= (upper_sum_set (f + g)) . D by Def11;
hence ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_integral (f + g) by A23, XXREAL_0:2; :: thesis:

end;

A25: dom (upper_sum_set (f + g)) = divs A by FUNCT_2:def 1;
A26: for a1 being real number st a1 in rng (upper_sum_set f) holds
a1 >= (upper_integral (f + g)) - (upper_integral g)

proof

let a1 be real number ; :: 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
A28: a1 = (upper_sum_set f) . D1 by PARTFUN1:3;
reconsider D1 = D1 as Division of A by Def3;
A29: a1 = upper_sum (f,D1) by A28, Def11;
for a2 being real number st a2 in rng (upper_sum_set g) holds
a2 >= (upper_integral (f + g)) - a1

proof

let a2 be real number ; :: 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
A31: a2 = (upper_sum_set g) . D2 by PARTFUN1:3;
reconsider D2 = D2 as Division of A by Def3;
consider D being Division of A such that
A32: D1 <= D and
A33: D2 <= D by Th49;
A34: D in divs A by Def3;
(upper_sum_set g) . D = upper_sum (g,D) by Def11;
then A35: (upper_sum_set g) . D <= upper_sum (g,D2) by A2, A33, Th47;
(upper_sum_set f) . D = upper_sum (f,D) by Def11;
then (upper_sum_set f) . D <= upper_sum (f,D1) by A1, A32, Th47;
then A36: ((upper_sum_set f) . D) + ((upper_sum_set g) . D) <= (upper_sum (f,D1)) + (upper_sum (g,D2)) by A35, XREAL_1:7;
((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_integral (f + g) by A25, A18, A34;
then A37: (upper_sum (f,D1)) + (upper_sum (g,D2)) >= upper_integral (f + g) by A36, XXREAL_0:2;
a2 = upper_sum (g,D2) by A31, Def11;
hence a2 >= (upper_integral (f + g)) - a1 by A29, A37, 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 A26, SEQ_4:43;
then A38: (integral f) + (upper_integral g) >= upper_integral (f + g) by XREAL_1:20;
A39: 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:
A40: D in divs A by Def3;
(lower_sum (f,D)) + (lower_sum (g,D)) <= lower_sum ((f + g),D) by A1, A2, Th58;
then A42: ((lower_sum_set f) . D) + (lower_sum (g,D)) <= lower_sum ((f + g),D) by Def12;
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 A44: (lower_sum_set (f + g)) . D <= lower_integral (f + g) by A11, SEQ_4:def 1;
((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_sum ((f + g),D) by A42, Def12;
then ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= (lower_sum_set (f + g)) . D by Def12;
hence ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_integral (f + g) by A44, XXREAL_0:2; :: thesis:

end;

A46: dom (lower_sum_set (f + g)) = divs A by FUNCT_2:def 1;
A47: for a1 being real number st a1 in rng (lower_sum_set f) holds
a1 <= (lower_integral (f + g)) - (lower_integral g)

proof

let a1 be real number ; :: 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
A49: a1 = (lower_sum_set f) . D1 by PARTFUN1:3;
reconsider D1 = D1 as Division of A by Def3;
A50: a1 = lower_sum (f,D1) by A49, Def12;
for a2 being real number st a2 in rng (lower_sum_set g) holds
a2 <= (lower_integral (f + g)) - a1

proof

let a2 be real number ; :: 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
A52: a2 = (lower_sum_set g) . D2 by PARTFUN1:3;
reconsider D2 = D2 as Division of A by Def3;
consider D being Division of A such that
A53: D1 <= D and
A54: D2 <= D by Th49;
A55: D in divs A by Def3;
(lower_sum_set g) . D = lower_sum (g,D) by Def12;
then A56: (lower_sum_set g) . D >= lower_sum (g,D2) by A2, A54, Th48;
(lower_sum_set f) . D = lower_sum (f,D) by Def12;
then (lower_sum_set f) . D >= lower_sum (f,D1) by A1, A53, Th48;
then A57: ((lower_sum_set f) . D) + ((lower_sum_set g) . D) >= (lower_sum (f,D1)) + (lower_sum (g,D2)) by A56, XREAL_1:7;
((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_integral (f + g) by A46, A39, A55;
then A58: (lower_sum (f,D1)) + (lower_sum (g,D2)) <= lower_integral (f + g) by A57, XXREAL_0:2;
a2 = lower_sum (g,D2) by A52, Def12;
hence a2 <= (lower_integral (f + g)) - a1 by A50, A58, 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 A47, SEQ_4:45;
then A59: (lower_integral f) + (lower_integral g) <= lower_integral (f + g) by XREAL_1:19;
A60: upper_integral (f + g) >= lower_integral (f + g) by A6, Th51;
then (integral f) + (integral g) <= upper_integral (f + g) by A59, A5, XXREAL_0:2;
then upper_integral (f + g) = (integral f) + (integral g) by A38, XXREAL_0:1;
then A61: upper_integral (f + g) = lower_integral (f + g) by A59, A60, A5, XXREAL_0:1;
f + g is upper_integrable by A17, Def13;
hence ( f + g is integrable & integral (f + g) = (integral f) + (integral g) ) by A12, A59, A5, A38, A61, Def17, XXREAL_0:1; :: thesis: