let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for f, g being Function of A,REAL st f | A is bounded_above & g | A is bounded_above holds
upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D))
let D be Division of A; :: thesis: for f, g being Function of A,REAL st f | A is bounded_above & g | A is bounded_above holds
upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D))
let f, g be Function of A,REAL; :: thesis: ( f | A is bounded_above & g | A is bounded_above implies upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D)) )
assume that
A1: f | A is bounded_above and
A2: g | A is bounded_above ; :: thesis: upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D))
set H = upper_volume ((f + g),D);
set G = upper_volume (g,D);
set F = upper_volume (f,D);
len (upper_volume (g,D)) = len D by Def5;
then A3: upper_volume (g,D) is Element of (len D) -tuples_on REAL by FINSEQ_2:92;
len (upper_volume (f,D)) = len D by Def5;
then A4: upper_volume (f,D) is Element of (len D) -tuples_on REAL by FINSEQ_2:92;
A5: for j being Nat st j in Seg (len D) holds
(upper_volume ((f + g),D)) . j <= ((upper_volume (f,D)) + (upper_volume (g,D))) . j

proof

let j be Nat; :: thesis: ( j in Seg (len D) implies (upper_volume ((f + g),D)) . j <= ((upper_volume (f,D)) + (upper_volume (g,D))) . j )
assume j in Seg (len D) ; :: thesis: (upper_volume ((f + g),D)) . j <= ((upper_volume (f,D)) + (upper_volume (g,D))) . j
then j in dom D by FINSEQ_1:def 3;
then (upper_volume ((f + g),D)) . j <= ((upper_volume (f,D)) . j) + ((upper_volume (g,D)) . j) by A1, A2, Th51;
hence (upper_volume ((f + g),D)) . j <= ((upper_volume (f,D)) + (upper_volume (g,D))) . j by A4, A3, RVSUM_1:11; :: thesis: verum

end;

len (upper_volume ((f + g),D)) = len D by Def5;
then A6: upper_volume ((f + g),D) is Element of (len D) -tuples_on REAL by FINSEQ_2:92;
(upper_volume (f,D)) + (upper_volume (g,D)) is Element of (len D) -tuples_on REAL by A4, A3, FINSEQ_2:120;
then Sum (upper_volume ((f + g),D)) <= Sum ((upper_volume (f,D)) + (upper_volume (g,D))) by A6, A5, RVSUM_1:82;
hence upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D)) by A4, A3, RVSUM_1:89; :: thesis: verum