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_below & g | A is bounded_below holds
(lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D
let D be Division of A; :: thesis: for f, g being Function of A,REAL st f | A is bounded_below & g | A is bounded_below holds
(lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D
let f, g be Function of A,REAL ; :: thesis: ( f | A is bounded_below & g | A is bounded_below implies (lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D )
assume A1: ( f | A is bounded_below & g | A is bounded_below ) ; :: thesis: (lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D
set F = lower_volume f,D;
set G = lower_volume g,D;
set H = lower_volume (f + g),D;
A2: len (lower_volume f,D) = len D by Def8;
A3: len (lower_volume g,D) = len D by Def8;
A4: len (lower_volume (f + g),D) = len D by Def8;
A5: lower_volume f,D is Element of (len D) -tuples_on REAL by A2, FINSEQ_2:110;
A6: lower_volume g,D is Element of (len D) -tuples_on REAL by A3, FINSEQ_2:110;
A7: lower_volume (f + g),D is Element of (len D) -tuples_on REAL by A4, FINSEQ_2:110;
A8: (lower_volume f,D) + (lower_volume g,D) is Element of (len D) -tuples_on REAL by A5, A6, FINSEQ_2:140;
for j being Nat st j in Seg (len D) holds
((lower_volume f,D) + (lower_volume g,D)) . j <= (lower_volume (f + g),D) . j

proof

let j be Nat; :: thesis: ( j in Seg (len D) implies ((lower_volume f,D) + (lower_volume g,D)) . j <= (lower_volume (f + g),D) . j )
assume j in Seg (len D) ; :: thesis: ((lower_volume f,D) + (lower_volume g,D)) . j <= (lower_volume (f + g),D) . j
then j in dom D by FINSEQ_1:def 3;
then ((lower_volume f,D) . j) + ((lower_volume g,D) . j) <= (lower_volume (f + g),D) . j by A1, Th56;
hence ((lower_volume f,D) + (lower_volume g,D)) . j <= (lower_volume (f + g),D) . j by A5, A6, RVSUM_1:27; :: thesis: verum

end;

then Sum ((lower_volume f,D) + (lower_volume g,D)) <= Sum (lower_volume (f + g),D) by A7, A8, RVSUM_1:112;
hence (lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D by A5, A6, RVSUM_1:119; :: thesis: verum