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_below & g | A is bounded_below holds
((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + 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_below & g | A is bounded_below holds
((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + 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_below & g | A is bounded_below holds
((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + 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_below & g | A is bounded_below holds
((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i
let D be Element of S; :: thesis: ( i in dom D & f | A is bounded_below & g | A is bounded_below implies ((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i )
assume A1:
i in dom D
; :: thesis: ( not f | A is bounded_below or not g | A is bounded_below or ((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i )
assume A2:
f | A is bounded_below
; :: thesis: ( not g | A is bounded_below or ((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i )
assume A3:
g | A is bounded_below
; :: thesis: ((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i
A4:
( rng (f | (divset D,i)) is bounded_below & 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_below
by A2, Th13;
hence
rng (f | (divset D,i)) is
bounded_below
by X, XXREAL_2:44;
:: 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_below & 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_below
by A3, Th13;
hence
rng (g | (divset D,i)) is
bounded_below
by X, XXREAL_2:44;
:: 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:
lower_bound ((rng (f | (divset D,i))) + (rng (g | (divset D,i)))) = (lower_bound (rng (f | (divset D,i)))) + (lower_bound (rng (g | (divset D,i))))
by A4, COMPLSP1:96;
A9:
(rng (f | (divset D,i))) + (rng (g | (divset D,i))) is bounded_below
by A4, A6, COMPLSP1:95;
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
(lower_bound (rng ((f + g) | (divset D,i)))) * (vol (divset D,i)) >= ((lower_bound (rng (f | (divset D,i)))) + (lower_bound (rng (g | (divset D,i))))) * (vol (divset D,i))
by A8, A9, A10, A12, SEQ_4:64, XREAL_1:66;
then
(lower_volume (f + g),D) . i >= ((lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i))) + ((lower_bound (rng (g | (divset D,i)))) * (vol (divset D,i)))
by A1, Def8;
then
(lower_volume (f + g),D) . i >= ((lower_volume f,D) . i) + ((lower_bound (rng (g | (divset D,i)))) * (vol (divset D,i)))
by A1, Def8;
hence
((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i
by A1, Def8; :: thesis: verum