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_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 Def6;
then A3: lower_volume (g,D) is Element of (len D) -tuples_on REAL by FINSEQ_2:92;
len (lower_volume (f,D)) = len D by Def6;
then A4: lower_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
((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, Th52;
hence ((lower_volume (f,D)) + (lower_volume (g,D))) . j <= (lower_volume ((f + g),D)) . j by A4, A3, RVSUM_1:11; :: thesis: verum

end;

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