let A be 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 Def7;
then A3: upper_volume g,D is Element of (len D) -tuples_on REAL by FINSEQ_2:110;
len (upper_volume f,D) = len D by Def7;
then A4: upper_volume f,D is Element of (len D) -tuples_on REAL by FINSEQ_2:110;
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, Th55;
hence (upper_volume (f + g),D) . j <= ((upper_volume f,D) + (upper_volume g,D)) . j by A4, A3, RVSUM_1:27; :: thesis: verum

end;

len (upper_volume (f + g),D) = len D by Def7;
then A6: upper_volume (f + g),D is Element of (len D) -tuples_on REAL by FINSEQ_2:110;
(upper_volume f,D) + (upper_volume g,D) is Element of (len D) -tuples_on REAL by A4, A3, FINSEQ_2:140;
then Sum (upper_volume (f + g),D) <= Sum ((upper_volume f,D) + (upper_volume g,D)) by A6, A5, RVSUM_1:112;
hence upper_sum (f + g),D <= (upper_sum f,D) + (upper_sum g,D) by A4, A3, RVSUM_1:119; :: thesis: verum