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 that
A1: f | A is bounded_below and
A2: g | A is bounded_below ; :: thesis: (lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D
set H = lower_volume (f + g),D;
set G = lower_volume g,D;
set F = lower_volume f,D;
len (lower_volume g,D) = len D by Def8;
then A3: lower_volume g,D is Element of (len D) -tuples_on REAL by FINSEQ_2:110;
len (lower_volume f,D) = len D by Def8;
then A4: lower_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
((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, A2, Th56;
hence ((lower_volume f,D) + (lower_volume g,D)) . j <= (lower_volume (f + g),D) . j by A4, A3, RVSUM_1:27; :: thesis: verum

end;

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