let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for f, g being Function of A, REAL
for S being non empty Division of A
for D being Element of S st i in dom D & f | A is bounded_above & g | A is bounded_above holds
(upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i)
let A be closed-interval Subset of REAL ; :: thesis: for f, g being Function of A, REAL
for S being non empty Division of A
for D being Element of S st i in dom D & f | A is bounded_above & g | A is bounded_above holds
(upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i)
let f, g be Function of A, REAL ; :: thesis: for S being non empty Division of A
for D being Element of S st i in dom D & f | A is bounded_above & g | A is bounded_above holds
(upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i)
let S be non empty Division of A; :: thesis: for D being Element of S st i in dom D & f | A is bounded_above & g | A is bounded_above holds
(upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i)
let D be Element of S; :: thesis: ( i in dom D & f | A is bounded_above & g | A is bounded_above implies (upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i) )
assume A1:
i in dom D
; :: thesis: ( not f | A is bounded_above or not g | A is bounded_above or (upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i) )
assume A2:
f | A is bounded_above
; :: thesis: ( not g | A is bounded_above or (upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i) )
assume A3:
g | A is bounded_above
; :: thesis: (upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i)
A4:
( rng (f | (divset D,i)) is bounded_above & not rng (f | (divset D,i)) is empty )
proof
X:
rng (f | (divset D,i)) c= rng f
by RELAT_1:99;
rng f is
bounded_above
by A2, Th15;
hence
rng (f | (divset D,i)) is
bounded_above
by X, XXREAL_2:43;
:: thesis: not rng (f | (divset D,i)) is empty
A5:
dom f = A
by FUNCT_2:def 1;
dom (f | (divset D,i)) = divset D,
i
by A5, Th10, A1, RELAT_1:91;
hence
not
rng (f | (divset D,i)) is
empty
by RELAT_1:65;
:: thesis: verum
end;
A6:
( rng (g | (divset D,i)) is bounded_above & not rng (g | (divset D,i)) is empty )
proof
X:
rng (g | (divset D,i)) c= rng g
by RELAT_1:99;
rng g is
bounded_above
by A3, Th15;
hence
rng (g | (divset D,i)) is
bounded_above
by X, XXREAL_2:43;
:: thesis: not rng (g | (divset D,i)) is empty
A7:
dom g = A
by FUNCT_2:def 1;
dom (g | (divset D,i)) = divset D,
i
by A7, Th10, A1, RELAT_1:91;
hence
not
rng (g | (divset D,i)) is
empty
by RELAT_1:65;
:: thesis: verum
end;
then A8:
upper_bound ((rng (f | (divset D,i))) + (rng (g | (divset D,i)))) = (upper_bound (rng (f | (divset D,i)))) + (upper_bound (rng (g | (divset D,i))))
by A4, Th54;
A9:
(rng (f | (divset D,i))) + (rng (g | (divset D,i))) is bounded_above
by A4, A6, Th53;
A10:
not rng ((f + g) | (divset D,i)) is empty
A12:
0 <= vol (divset D,i)
by SEQ_4:24, XREAL_1:50;
(f + g) | (divset D,i) = (f | (divset D,i)) + (g | (divset D,i))
by RFUNCT_1:60;
then
rng ((f + g) | (divset D,i)) c= (rng (f | (divset D,i))) + (rng (g | (divset D,i)))
by Th12;
then
(upper_bound (rng ((f + g) | (divset D,i)))) * (vol (divset D,i)) <= ((upper_bound (rng (f | (divset D,i)))) + (upper_bound (rng (g | (divset D,i))))) * (vol (divset D,i))
by A8, A9, A10, A12, SEQ_4:65, XREAL_1:66;
then
(upper_volume (f + g),D) . i <= ((upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i))) + ((upper_bound (rng (g | (divset D,i)))) * (vol (divset D,i)))
by A1, Def7;
then
(upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_bound (rng (g | (divset D,i)))) * (vol (divset D,i)))
by A1, Def7;
hence
(upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i)
by A1, Def7; :: thesis: verum