let A be non empty closed_interval Subset of REAL; 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; 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; ( 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
; (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;
( 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)
;
((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;
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; verum