let A be 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: ( f | A is bounded_above & f | A is bounded_below ) by A1;
A6: ( g | A is bounded_above & g | A is bounded_below ) by A2;
A7: (f + g) | (A /\ A) is bounded by A1, A2, RFUNCT_1:100;
A8: dom (upper_sum_set (f + g)) = divs A by Def11;
A9: dom (lower_sum_set (f + g)) = divs A by Def12;
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 A10: D in (divs A) /\ (dom (upper_sum_set (f + g))) ; :: thesis:
then reconsider D = D as Division of A by Def3;
D in dom (upper_sum_set (f + g)) by A10, XBOOLE_0:def 4;
then (upper_sum_set (f + g)) . D = upper_sum (f + g),D by Def11;
then A11: lower_sum (f + g),D <= (upper_sum_set (f + g)) . D by A7, Th30;
(lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D by A5, A6, Th58;
then A12: (lower_sum f,D) + (lower_sum g,D) <= (upper_sum_set (f + g)) . D by A11, XXREAL_0:2;
((lower_bound (rng f)) * (vol A)) + (lower_sum g,D) <= (lower_sum f,D) + (lower_sum g,D)

proof

(lower_bound (rng f)) * (vol A) <= lower_sum f,D by A5, Th27;
hence ((lower_bound (rng f)) * (vol A)) + (lower_sum g,D) <= (lower_sum f,D) + (lower_sum g,D) by XREAL_1:8; :: thesis:

end;

then A13: ((lower_bound (rng f)) * (vol A)) + (lower_sum g,D) <= (upper_sum_set (f + g)) . D by A12, XXREAL_0:2;
((lower_bound (rng f)) * (vol A)) + ((lower_bound (rng g)) * (vol A)) <= ((lower_bound (rng f)) * (vol A)) + (lower_sum g,D)

proof

(lower_bound (rng g)) * (vol A) <= lower_sum g,D by A6, Th27;
hence ((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:8; :: thesis:

end;

hence ((lower_bound (rng f)) * (vol A)) + ((lower_bound (rng g)) * (vol A)) <= (upper_sum_set (f + g)) . D by A13, XXREAL_0:2; :: thesis:

end;

then (upper_sum_set (f + g)) | (divs A) is bounded_below by RFUNCT_1:88;
then A14: rng (upper_sum_set (f + g)) is bounded_below by Th13;
then A15: f + g is upper_integrable by Def13;
A16: rng (lower_sum_set (f + g)) is bounded_above

proof

(lower_sum_set (f + g)) | (divs A) is bounded_above

proof

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 A17: D in (divs A) /\ (dom (lower_sum_set (f + g))) ; :: thesis:
then reconsider D = D as Division of A by Def3;
D in dom (lower_sum_set (f + g)) by A17, XBOOLE_0:def 4;
then (lower_sum_set (f + g)) . D = lower_sum (f + g),D by Def12;
then A18: (lower_sum_set (f + g)) . D <= upper_sum (f + g),D by A7, Th30;
upper_sum (f + g),D <= (upper_sum f,D) + (upper_sum g,D) by A5, A6, Th57;
then A19: (lower_sum_set (f + g)) . D <= (upper_sum f,D) + (upper_sum g,D) by A18, XXREAL_0:2;
(upper_sum f,D) + (upper_sum g,D) <= ((upper_bound (rng f)) * (vol A)) + (upper_sum g,D)

proof

upper_sum f,D <= (upper_bound (rng f)) * (vol A) by A5, Th29;
hence (upper_sum f,D) + (upper_sum g,D) <= ((upper_bound (rng f)) * (vol A)) + (upper_sum g,D) by XREAL_1:8; :: thesis:

end;

then A20: (lower_sum_set (f + g)) . D <= ((upper_bound (rng f)) * (vol A)) + (upper_sum g,D) by A19, XXREAL_0:2;
((upper_bound (rng f)) * (vol A)) + (upper_sum g,D) <= ((upper_bound (rng f)) * (vol A)) + ((upper_bound (rng g)) * (vol A))

proof

upper_sum g,D <= (upper_bound (rng g)) * (vol A) by A6, Th29;
hence ((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:8; :: thesis:

end;

hence (lower_sum_set (f + g)) . D <= ((upper_bound (rng f)) * (vol A)) + ((upper_bound (rng g)) * (vol A)) by A20, XXREAL_0:2; :: thesis:

end;

hence (lower_sum_set (f + g)) | (divs A) is bounded_above by RFUNCT_1:87; :: thesis:

end;

hence rng (lower_sum_set (f + g)) is bounded_above by Th15; :: thesis:

end;

then A21: f + g is lower_integrable by Def14;
( upper_integral (f + g) = lower_integral (f + g) & upper_integral (f + g) = (integral f) + (integral g) )

proof

dom (upper_sum_set f) <> {} by Def11;
then A22: rng (upper_sum_set f) is non empty Subset of REAL by RELAT_1:65;
dom (lower_sum_set f) <> {} by Def12;
then A23: rng (lower_sum_set f) is non empty Subset of REAL by RELAT_1:65;
dom (upper_sum_set g) <> {} by Def11;
then A24: rng (upper_sum_set g) is non empty Subset of REAL by RELAT_1:65;
dom (lower_sum_set g) <> {} by Def12;
then A25: rng (lower_sum_set g) is non empty Subset of REAL by RELAT_1:65;
A26: 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:
assume D in (divs A) /\ (dom (upper_sum_set (f + g))) ; :: thesis:
then A27: 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 5;
then A28: (upper_sum_set (f + g)) . D >= upper_integral (f + g) by A14, SEQ_4:def 5;
A29: ( D in dom (upper_sum_set f) & D in dom (upper_sum_set g) )

proof

A30: D in divs A by Def3;
hence D in dom (upper_sum_set f) by Def11; :: thesis:
thus D in dom (upper_sum_set g) by A30, Def11; :: thesis:

end;

(upper_sum f,D) + (upper_sum g,D) >= upper_sum (f + g),D by A5, A6, Th57;
then ((upper_sum_set f) . D) + (upper_sum g,D) >= upper_sum (f + g),D by A29, Def11;
then ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_sum (f + g),D by A29, Def11;
then ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= (upper_sum_set (f + g)) . D by A27, Def11;
hence ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_integral (f + g) by A28, XXREAL_0:2; :: thesis:

end;

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:
assume D in (divs A) /\ (dom (lower_sum_set (f + g))) ; :: thesis:
then A32: 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 5;
then A33: (lower_sum_set (f + g)) . D <= lower_integral (f + g) by A16, SEQ_4:def 4;
A34: ( D in dom (lower_sum_set f) & D in dom (lower_sum_set g) )

proof

A35: D in divs A by Def3;
hence D in dom (lower_sum_set f) by Def12; :: thesis:
thus D in dom (lower_sum_set g) by A35, Def12; :: thesis:

end;

(lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D by A5, A6, Th58;
then ((lower_sum_set f) . D) + (lower_sum g,D) <= lower_sum (f + g),D by A34, Def12;
then ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_sum (f + g),D by A34, Def12;
then ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= (lower_sum_set (f + g)) . D by A32, Def12;
hence ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_integral (f + g) by A33, XXREAL_0:2; :: thesis:

end;

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
A36: ( D1 in dom (upper_sum_set f) & a1 = (upper_sum_set f) . D1 ) by PARTFUN1:26;
reconsider D1 = D1 as Division of A by Def3;
A37: a1 = upper_sum f,D1 by A36, 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
A38: ( D2 in dom (upper_sum_set g) & a2 = (upper_sum_set g) . D2 ) by PARTFUN1:26;
reconsider D2 = D2 as Division of A by Def3;
A39: a2 = upper_sum g,D2 by A38, Def11;
consider D being Division of A such that
A40: ( D1 <= D & D2 <= D ) by Th49;
A43: D in divs A by Def3;
then A41: ((upper_sum_set f) . D) + ((upper_sum_set g) . D) >= upper_integral (f + g) by A8, A26;
A42: ( D in dom (upper_sum_set f) & D in dom (upper_sum_set g) ) by A43, Def11;
then (upper_sum_set f) . D = upper_sum f,D by Def11;
then A44: (upper_sum_set f) . D <= upper_sum f,D1 by A5, A40, Th47;
(upper_sum_set g) . D = upper_sum g,D by A42, Def11;
then (upper_sum_set g) . D <= upper_sum g,D2 by A6, A40, Th47;
then ((upper_sum_set f) . D) + ((upper_sum_set g) . D) <= (upper_sum f,D1) + (upper_sum g,D2) by A44, XREAL_1:9;
then (upper_sum f,D1) + (upper_sum g,D2) >= upper_integral (f + g) by A41, XXREAL_0:2;
hence a2 >= (upper_integral (f + g)) - a1 by A37, A39, XREAL_1:22; :: thesis:

end;

then lower_bound (rng (upper_sum_set g)) >= (upper_integral (f + g)) - a1 by A24, SEQ_4:60;
then a1 + (lower_bound (rng (upper_sum_set g))) >= upper_integral (f + g) by XREAL_1:22;
hence a1 >= (upper_integral (f + g)) - (upper_integral g) by XREAL_1:22; :: thesis:

end;

then A45: upper_integral f >= (upper_integral (f + g)) - (upper_integral g) by A22, SEQ_4:60;
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
A46: ( D1 in dom (lower_sum_set f) & a1 = (lower_sum_set f) . D1 ) by PARTFUN1:26;
reconsider D1 = D1 as Division of A by Def3;
A47: a1 = lower_sum f,D1 by A46, 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
A48: ( D2 in dom (lower_sum_set g) & a2 = (lower_sum_set g) . D2 ) by PARTFUN1:26;
reconsider D2 = D2 as Division of A by Def3;
A49: a2 = lower_sum g,D2 by A48, Def12;
consider D being Division of A such that
A50: ( D1 <= D & D2 <= D ) by Th49;
A53: D in divs A by Def3;
then A51: ((lower_sum_set f) . D) + ((lower_sum_set g) . D) <= lower_integral (f + g) by A9, A31;
A52: ( D in dom (lower_sum_set f) & D in dom (lower_sum_set g) ) by A53, Def12;
then (lower_sum_set f) . D = lower_sum f,D by Def12;
then A54: (lower_sum_set f) . D >= lower_sum f,D1 by A5, A50, Th48;
(lower_sum_set g) . D = lower_sum g,D by A52, Def12;
then (lower_sum_set g) . D >= lower_sum g,D2 by A6, A50, Th48;
then ((lower_sum_set f) . D) + ((lower_sum_set g) . D) >= (lower_sum f,D1) + (lower_sum g,D2) by A54, XREAL_1:9;
then (lower_sum f,D1) + (lower_sum g,D2) <= lower_integral (f + g) by A51, XXREAL_0:2;
hence a2 <= (lower_integral (f + g)) - a1 by A47, A49, XREAL_1:21; :: thesis:

end;

then upper_bound (rng (lower_sum_set g)) <= (lower_integral (f + g)) - a1 by A25, SEQ_4:62;
then a1 + (upper_bound (rng (lower_sum_set g))) <= lower_integral (f + g) by XREAL_1:21;
hence a1 <= (lower_integral (f + g)) - (lower_integral g) by XREAL_1:21; :: thesis:

end;

then upper_bound (rng (lower_sum_set f)) <= (lower_integral (f + g)) - (lower_integral g) by A23, SEQ_4:62;
then A55: (lower_integral f) + (lower_integral g) <= lower_integral (f + g) by XREAL_1:21;
A56: upper_integral (f + g) >= lower_integral (f + g) by A7, Th51;
A57: (lower_integral f) + (lower_integral g) = (upper_integral f) + (lower_integral g) by A3, Def17
.= (integral f) + (integral g) by A4, Def17 ;
then A58: (integral f) + (integral g) <= upper_integral (f + g) by A55, A56, XXREAL_0:2;
(integral f) + (upper_integral g) >= upper_integral (f + g) by A45, XREAL_1:22;
then upper_integral (f + g) = (integral f) + (integral g) by A58, XXREAL_0:1;
hence ( upper_integral (f + g) = lower_integral (f + g) & upper_integral (f + g) = (integral f) + (integral g) ) by A55, A56, A57, XXREAL_0:1; :: thesis:

end;

hence ( f + g is integrable & integral (f + g) = (integral f) + (integral g) ) by A15, A21, Def17; :: thesis: