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 being Function of A,REAL st f | A is bounded_above & i in dom D holds
(upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for f being Function of A,REAL st f | A is bounded_above & i in dom D holds
(upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
let D be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded_above & i in dom D holds
(upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
let f be Function of A,REAL; :: thesis: ( f | A is bounded_above & i in dom D implies (upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
A1: dom f = A by FUNCT_2:def 1;
assume f | A is bounded_above ; :: thesis: ( not i in dom D or (upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) )
then A2: rng f is bounded_above by Th11;
assume i in dom D ; :: thesis: (upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
then dom (f | (divset (D,i))) = divset (D,i) by A1, Th6, RELAT_1:62;
then A3: rng (f | (divset (D,i))) is non empty Subset of REAL by RELAT_1:42;
A4: 0 <= vol (divset (D,i)) by SEQ_4:11, XREAL_1:48;
rng (f | (divset (D,i))) c= rng f by RELAT_1:70;
hence (upper_bound (rng f)) * (vol (divset (D,i))) >= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A3, A2, A4, SEQ_4:48, XREAL_1:64; :: thesis: verum