let i be Element of NAT ; :: thesis: for A being non empty 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_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 non empty 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_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 Division of A; :: thesis: for f, g being Function of A,REAL 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: ( 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) )
dom (f + g) = A /\ A by FUNCT_2:def 1;
then dom ((f + g) | (divset (D,i))) = divset (D,i) by A1, Th6, RELAT_1:62;
then A2: not rng ((f + g) | (divset (D,i))) is empty by RELAT_1:42;
(f + g) | (divset (D,i)) = (f | (divset (D,i))) + (g | (divset (D,i))) by RFUNCT_1:44;
then A3: rng ((f + g) | (divset (D,i))) c= (rng (f | (divset (D,i)))) ++ (rng (g | (divset (D,i)))) by Th8;
assume 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) )
then rng f is bounded_above by Th11;
then A4: rng (f | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43;
dom g = A by FUNCT_2:def 1;
then dom (g | (divset (D,i))) = divset (D,i) by A1, Th6, RELAT_1:62;
then A5: not rng (g | (divset (D,i))) is empty by RELAT_1:42;
A6: 0 <= vol (divset (D,i)) by SEQ_4:11, XREAL_1:48;
assume g | A is bounded_above ; :: thesis: (upper_volume ((f + g),D)) . i <= ((upper_volume (f,D)) . i) + ((upper_volume (g,D)) . i)
then rng g is bounded_above by Th11;
then A7: rng (g | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43;
then A8: (rng (f | (divset (D,i)))) ++ (rng (g | (divset (D,i)))) is bounded_above by A4, Th49;
dom f = A by FUNCT_2:def 1;
then dom (f | (divset (D,i))) = divset (D,i) by A1, Th6, RELAT_1:62;
then not rng (f | (divset (D,i))) is empty by RELAT_1:42;
then 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, A7, A5, Th50;
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, A2, A6, A3, SEQ_4:48, XREAL_1:64;
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, Def5;
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, Def5;
hence (upper_volume ((f + g),D)) . i <= ((upper_volume (f,D)) . i) + ((upper_volume (g,D)) . i) by A1, Def5; :: thesis: verum