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_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; 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; ( 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
; 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 Def5;
then A3:
upper_volume (g,D) is Element of (len D) -tuples_on REAL
by FINSEQ_2:92;
len (upper_volume (f,D)) = len D
by Def5;
then A4:
upper_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
(upper_volume ((f + g),D)) . j <= ((upper_volume (f,D)) + (upper_volume (g,D))) . j
proof
let j be
Nat;
( 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)
;
(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, Th51;
hence
(upper_volume ((f + g),D)) . j <= ((upper_volume (f,D)) + (upper_volume (g,D))) . j
by A4, A3, RVSUM_1:11;
verum
end;
len (upper_volume ((f + g),D)) = len D
by Def5;
then A6:
upper_volume ((f + g),D) is Element of (len D) -tuples_on REAL
by FINSEQ_2:92;
(upper_volume (f,D)) + (upper_volume (g,D)) is Element of (len D) -tuples_on REAL
by A4, A3, FINSEQ_2:120;
then
Sum (upper_volume ((f + g),D)) <= Sum ((upper_volume (f,D)) + (upper_volume (g,D)))
by A6, A5, RVSUM_1:82;
hence
upper_sum ((f + g),D) <= (upper_sum (f,D)) + (upper_sum (g,D))
by A4, A3, RVSUM_1:89; verum