let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for D being Division of A
for f, g being Function of A,REAL 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 D being Division of A
for f, g being Function of A,REAL 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 Division of A; :: thesis: for f, g being Function of A,REAL 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: ( 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 that
A1: i in dom D and
A2: f | A is bounded_below and
A3: g | A is bounded_below ; :: thesis: ((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i
A4: 0 <= vol (divset D,i) by SEQ_4:24, XREAL_1:50;
dom (f + g) = A /\ A by FUNCT_2:def 1;
then dom ((f + g) | (divset D,i)) = divset D,i by A1, Th10, RELAT_1:91;
then A5: not rng ((f + g) | (divset D,i)) is empty by RELAT_1:65;
rng g is bounded_below by A3, Th13;
then A6: rng (g | (divset D,i)) is bounded_below by RELAT_1:99, XXREAL_2:44;
dom g = A by FUNCT_2:def 1;
then dom (g | (divset D,i)) = divset D,i by A1, Th10, RELAT_1:91;
then A7: not rng (g | (divset D,i)) is empty by RELAT_1:65;
(f + g) | (divset D,i) = (f | (divset D,i)) + (g | (divset D,i)) by RFUNCT_1:60;
then A8: rng ((f + g) | (divset D,i)) c= (rng (f | (divset D,i))) ++ (rng (g | (divset D,i))) by Th12;
rng f is bounded_below by A2, Th13;
then A9: rng (f | (divset D,i)) is bounded_below by RELAT_1:99, XXREAL_2:44;
then A10: (rng (f | (divset D,i))) ++ (rng (g | (divset D,i))) is bounded_below by A6, SEQ_4:141;
dom f = A by FUNCT_2:def 1;
then dom (f | (divset D,i)) = divset D,i by A1, Th10, RELAT_1:91;
then not rng (f | (divset D,i)) is empty by RELAT_1:65;
then 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 A9, A6, A7, SEQ_4:142;
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 A10, A5, A4, A8, 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